Proof
001. 1 ⊢ X = {x | x ∈ {∅, {∅}} ∧ (A ∨ x = ∅)}, hypo.
002. 2 ⊢ Y = {y | y ∈ {∅, {∅}} ∧ (A ∨ y = {∅})}, hypo.
003. ⊢ set ∅, empty_set_is_set.
004. ⊢ set {∅}, set_sg 3.
005. ⊢ ∅ ∈ {∅, {∅}}, in21 3.
006. ⊢ {∅} ∈ {∅, {∅}}, in22 4.
007. ⊢ u = u, eq_refl.
008. ⊢ A ∨ u = u, disj_intror 7.
009. ⊢ A ∨ ∅ = ∅, 8.
010. ⊢ A ∨ {∅} = {∅}, 8.
011. ⊢ ∅ ∈ {∅, {∅}} ∧ (A ∨ ∅ = ∅), conj_intro 5 9.
012. ⊢ {∅} ∈ {∅, {∅}} ∧ (A ∨ {∅} = {∅}), conj_intro 6 10.
013. ⊢ ∅ ∈ {x | x ∈ {∅, {∅}} ∧ (A ∨ x = ∅)}, comp_intro 3 11,
P x ↔ x ∈ {∅, {∅}} ∧ (A ∨ x = ∅).
014. ⊢ {∅} ∈ {y | y ∈ {∅, {∅}} ∧ (A ∨ y = {∅})}, comp_intro 4 12,
P y ↔ y ∈ {∅, {∅}} ∧ (A ∨ y = {∅}).
015. 1 ⊢ ∅ ∈ X, eq_subst_rev 1 13, P u ↔ ∅ ∈ u.
016. 2 ⊢ {∅} ∈ Y, eq_subst_rev 2 14, P u ↔ {∅} ∈ u.
017. ⊢ set {{∅}}, set_sg 4.
018. ⊢ set {∅, {∅}}, set_union 4 17.
019. ⊢ set {x | x ∈ {∅, {∅}} ∧ (A ∨ x = ∅)}, sep_is_set 18.
020. ⊢ set {y | y ∈ {∅, {∅}} ∧ (A ∨ y = {∅})}, sep_is_set 18.
021. 1 ⊢ set X, eq_subst_rev 1 19, P u ↔ set u.
022. 2 ⊢ set Y, eq_subst_rev 2 20, P u ↔ set u.
023. 23 ⊢ u ∈ {X, Y} ∩ {∅}, hypo.
024. 23 ⊢ u ∈ {∅}, intersection_elimr 23.
025. 23 ⊢ u = ∅, sg_elim 3 24.
026. 23 ⊢ u ∈ {X, Y}, intersection_eliml 23.
027. 23 ⊢ u ∈ {X} ∨ u ∈ {Y}, union_elim 26.
028. 28 ⊢ u ∈ {X}, hypo.
029. 1, 28 ⊢ u = X, sg_elim 21 28.
030. 1, 28 ⊢ X = u, eq_symm 29.
031. 1, 23, 28 ⊢ X = ∅, eq_trans 30 25.
032. 1, 23, 28 ⊢ ∅ ∈ ∅, eq_subst 31 15.
033. 1, 23, 28 ⊢ u ∈ ∅, empty_efq 32.
034. 34 ⊢ u ∈ {Y}, hypo.
035. 2, 34 ⊢ u = Y, sg_elim 22 34.
036. 2, 34 ⊢ Y = u, eq_symm 35.
037. 2, 23, 34 ⊢ Y = ∅, eq_trans 36 25.
038. 2, 23, 34 ⊢ {∅} ∈ ∅, eq_subst 37 16.
039. 2, 23, 34 ⊢ u ∈ ∅, empty_efq 38.
040. 1, 2, 23 ⊢ u ∈ ∅, disj_elim 27 33 39.
041. 1, 2 ⊢ u ∈ {X, Y} ∩ {∅} → u ∈ ∅, subj_intro 40.
042. 1, 2 ⊢ ∀u. u ∈ {X, Y} ∩ {∅} → u ∈ ∅, uq_intro 41.
043. 1, 2 ⊢ {X, Y} ∩ {∅} ⊆ ∅, incl_intro 42.
044. ⊢ ∅ ⊆ {X, Y} ∩ {∅}, empty_set_is_least.
045. 1, 2 ⊢ {X, Y} ∩ {∅} = ∅, incl_antisym 43 44.
046. 1, 2 ⊢ {X, Y} \ {∅} = {X, Y}, diff_disjoint 45.
047. 47 ⊢ ∀M. ∃f. choice_function f ∧ dom f = M \ {∅}, hypo.
048. 47 ⊢ ∃f. choice_function f ∧ dom f = {X, Y} \ {∅}, uq_elim 47.
049. 49 ⊢ choice_function f ∧ dom f = {X, Y} \ {∅}, hypo.
050. 49 ⊢ choice_function f, conj_eliml 49.
051. 49 ⊢ dom f = {X, Y} \ {∅}, conj_elimr 49.
052. 1, 2, 49 ⊢ dom f = {X, Y}, eq_trans 51 46.
053. 49 ⊢ function f ∧ ∀x. x ∈ dom f → app f x ∈ x,
choice_fn_unfold 50.
054. 49 ⊢ function f, conj_eliml 53.
055. 49 ⊢ ∀x. x ∈ dom f → app f x ∈ x, conj_elimr 53.
056. ⊢ {x | x ∈ {∅, {∅}} ∧ (A ∨ x = ∅)} ⊆ {∅, {∅}}, sep_is_subclass.
057. ⊢ {y | y ∈ {∅, {∅}} ∧ (A ∨ y = {∅})} ⊆ {∅, {∅}}, sep_is_subclass.
058. 1 ⊢ X ⊆ {∅, {∅}}, eq_subst_rev 1 56, P u ↔ u ⊆ {∅, {∅}}.
059. 2 ⊢ Y ⊆ {∅, {∅}}, eq_subst_rev 2 57, P u ↔ u ⊆ {∅, {∅}}.
060. 1 ⊢ X ∈ {X, Y}, in21 21.
061. 2 ⊢ Y ∈ {X, Y}, in22 22.
062. 1, 2, 49 ⊢ X ∈ dom f, eq_subst_rev 52 60, P u ↔ X ∈ u.
063. 1, 2, 49 ⊢ Y ∈ dom f, eq_subst_rev 52 61, P u ↔ Y ∈ u.
064. 1, 2, 49 ⊢ app f X ∈ X, uq_bounded_elim 55 62.
065. 1, 2, 49 ⊢ app f Y ∈ Y, uq_bounded_elim 55 63.
066. 1, 2, 49 ⊢ app f X ∈ {x | x ∈ {∅, {∅}} ∧ (A ∨ x = ∅)},
eq_subst 1 64, P u ↔ app f X ∈ u.
067. 1, 2, 49 ⊢ app f Y ∈ {y | y ∈ {∅, {∅}} ∧ (A ∨ y = {∅})},
eq_subst 2 65, P u ↔ app f Y ∈ u.
068. 1, 2, 49 ⊢ app f X ∈ {∅, {∅}} ∧ (A ∨ app f X = ∅), comp_elim 66.
069. 1, 2, 49 ⊢ app f Y ∈ {∅, {∅}} ∧ (A ∨ app f Y = {∅}), comp_elim 67.
070. 1, 2, 49 ⊢ A ∨ app f X = ∅, conj_elimr 68.
071. 1, 2, 49 ⊢ A ∨ app f Y = {∅}, conj_elimr 69.
072. 1, 2, 49 ⊢ app f X ∈ {∅, {∅}}, conj_eliml 68.
073. 1, 2, 49 ⊢ app f Y ∈ {∅, {∅}}, conj_eliml 69.
074. 1, 2, 49 ⊢ app f X ∈ {∅} ∨ app f X ∈ {{∅}}, union_elim 72.
075. 1, 2, 49 ⊢ app f Y ∈ {∅} ∨ app f Y ∈ {{∅}}, union_elim 73.
076. 76 ⊢ app f Y ∈ {∅}, hypo.
077. 76 ⊢ app f Y = ∅, sg_elim 3 76.
078. 1, 2, 49, 76 ⊢ A ∨ ∅ = {∅}, eq_subst 77 71, P u ↔ A ∨ u = {∅}.
079. 1, 2, 49, 76 ⊢ A, tollendo_ponens_left 78 zero_neq_one.
080. 1, 2, 49, 76 ⊢ A ∨ ¬A, disj_introl 79.
081. 81 ⊢ app f Y ∈ {{∅}}, hypo.
082. 81 ⊢ app f Y = {∅}, sg_elim 4 81.
083. 83 ⊢ app f X ∈ {∅}, hypo.
084. 83 ⊢ app f X = ∅, sg_elim 3 83.
085. 85 ⊢ A, hypo.
086. 86 ⊢ u ∈ X, hypo.
087. 1, 86 ⊢ u ∈ {x | x ∈ {∅, {∅}} ∧ (A ∨ x = ∅)}, eq_subst 1 86.
088. 1, 86 ⊢ u ∈ {∅, {∅}} ∧ (A ∨ u = ∅), comp_elim 87.
089. 1, 86 ⊢ u ∈ {∅, {∅}}, conj_eliml 88.
090. 85 ⊢ A ∨ u = {∅}, disj_introl 85.
091. 1, 85, 86 ⊢ u ∈ {∅, {∅}} ∧ (A ∨ u = {∅}), conj_intro 89 90.
092. 1, 86 ⊢ set u, set_intro 89.
093. 1, 85, 86 ⊢ u ∈ {y | y ∈ {∅, {∅}} ∧ (A ∨ y = {∅})}, comp_intro 92 91.
094. 1, 2, 85, 86 ⊢ u ∈ Y, eq_subst_rev 2 93, P t ↔ u ∈ t.
095. 1, 2, 85 ⊢ u ∈ X → u ∈ Y, subj_intro 94.
096. 96 ⊢ u ∈ Y, hypo.
097. 2, 96 ⊢ u ∈ {y | y ∈ {∅, {∅}} ∧ (A ∨ y = {∅})}, eq_subst 2 96.
098. 2, 96 ⊢ u ∈ {∅, {∅}} ∧ (A ∨ u = {∅}), comp_elim 97.
099. 2, 96 ⊢ u ∈ {∅, {∅}}, conj_eliml 98.
100. 85 ⊢ A ∨ u = ∅, disj_introl 85.
101. 2, 85, 96 ⊢ u ∈ {∅, {∅}} ∧ (A ∨ u = ∅), conj_intro 99 100.
102. 2, 96 ⊢ set u, set_intro 99.
103. 2, 85, 96 ⊢ u ∈ {x | x ∈ {∅, {∅}} ∧ (A ∨ x = ∅)}, comp_intro 102 101.
104. 1, 2, 85, 96 ⊢ u ∈ X, eq_subst_rev 1 103, P t ↔ u ∈ t.
105. 1, 2, 85 ⊢ u ∈ Y → u ∈ X, subj_intro 104.
106. 1, 2, 85 ⊢ u ∈ X ↔ u ∈ Y, bij_intro 95 105.
107. 1, 2, 85 ⊢ ∀u. u ∈ X ↔ u ∈ Y, uq_intro 106.
108. 1, 2, 85 ⊢ X = Y, ext 107.
109. 1, 2, 85 ⊢ app f X = app f Y, f_equal 108, g x = app f x.
110. 83 ⊢ ∅ = app f X, eq_symm 84.
111. 1, 2, 83, 85 ⊢ ∅ = app f Y, eq_trans 110 109.
112. 1, 2, 81, 83, 85 ⊢ ∅ = {∅}, eq_trans 111 82.
113. 1, 2, 81, 83, 85 ⊢ ⊥, neg_elim zero_neq_one 112.
114. 1, 2, 81, 83 ⊢ ¬A, neg_intro 113.
115. 1, 2, 81, 83 ⊢ A ∨ ¬A, disj_intror 114.
116. 116 ⊢ app f X ∈ {{∅}}, hypo.
117. 116 ⊢ app f X = {∅}, sg_elim 4 116.
118. 1, 2, 49, 116 ⊢ A ∨ {∅} = ∅, eq_subst 117 70, P u ↔ A ∨ u = ∅.
119. ⊢ ¬{∅} = ∅, neq_symm zero_neq_one.
120. 1, 2, 49, 116 ⊢ A, tollendo_ponens_left 118 119.
121. 1, 2, 49, 116 ⊢ A ∨ ¬A, disj_introl 120.
122. 1, 2, 49, 81 ⊢ A ∨ ¬A, disj_elim 74 115 121.
123. 1, 2, 49 ⊢ A ∨ ¬A, disj_elim 75 80 122.
124. 47, 1, 2 ⊢ A ∨ ¬A, ex_elim 48 123.
125. 47, 1 ⊢ Y = {y | y ∈ {∅, {∅}} ∧ (A ∨ y = {∅})} → A ∨ ¬A,
subj_intro 124.
126. 47, 1 ⊢ ∀Y. Y = {y | y ∈ {∅, {∅}} ∧ (A ∨ y = {∅})} → A ∨ ¬A,
uq_intro 125.
127. 47, 1 ⊢ A ∨ ¬A, disused_eq 126.
128. 47 ⊢ X = {x | x ∈ {∅, {∅}} ∧ (A ∨ x = ∅)} → A ∨ ¬A,
subj_intro 127.
129. 47 ⊢ ∀X. X = {x | x ∈ {∅, {∅}} ∧ (A ∨ x = ∅)} → A ∨ ¬A,
uq_intro 128.
130. 47 ⊢ A ∨ ¬A, disused_eq 129.
Diaconescu_Goodman_Myhill_theorem. ⊢
(∀M. ∃f. choice_function f ∧ dom f = M \ {∅}) →
A ∨ ¬A, subj_intro 130.
Dependencies
The given proof depends on nine axioms:
comp, efq, eq_refl, eq_subst, ext, infinity, pairing, subset, union.