Home Intuitionistic Logic ExplorerTheorem List (p. 42 of 74) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 4101-4200   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremeqelsuc 4101 A set belongs to the successor of an equal set. (Contributed by NM, 18-Aug-1994.)
A V       (A = BA suc B)

Theoremiunsuc 4102* Inductive definition for the indexed union at a successor. (Contributed by Mario Carneiro, 4-Feb-2013.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
A V    &   (x = AB = 𝐶)        x suc AB = ( x A B𝐶)

TheoremsuctrALT 4103 The successor of a transtive class is transitive. (Contributed by Alan Sare, 11-Apr-2009.)
(Tr A → Tr suc A)

Theoremsuctr 4104 The sucessor of a transitive class is transitive. The proof of http://www.virtualdeduction.com/suctrvd.html is a Virtual Deduction proof verified by automatically transforming it into the Metamath proof of suctr 4104 using completeusersproof, which is verified by the Metamath program. The proof of http://www.virtualdeduction.com/suctrro.html is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. (Contributed by Alan Sare, 11-Apr-2009.) See suctrALT 4103 for the original proof before this revision. (Revised by Alan Sare, 12-Jun-2018.) (Proof modification is discouraged.)
(Tr A → Tr suc A)

Theoremtrsuc 4105 A set whose successor belongs to a transitive class also belongs. (Contributed by NM, 5-Sep-2003.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
((Tr A suc B A) → B A)

Theoremtrsucss 4106 A member of the successor of a transitive class is a subclass of it. (Contributed by NM, 4-Oct-2003.)
(Tr A → (B suc ABA))

Theoremsucssel 4107 A set whose successor is a subset of another class is a member of that class. (Contributed by NM, 16-Sep-1995.)
(A 𝑉 → (suc ABA B))

Theoremorduniss 4108 An ordinal class includes its union. (Contributed by NM, 13-Sep-2003.)
(Ord A AA)

Theoremonordi 4109 An ordinal number is an ordinal class. (Contributed by NM, 11-Jun-1994.)
A On       Ord A

Theoremontrci 4110 An ordinal number is a transitive class. (Contributed by NM, 11-Jun-1994.)
A On       Tr A

Theoremoneli 4111 A member of an ordinal number is an ordinal number. Theorem 7M(a) of [Enderton] p. 192. (Contributed by NM, 11-Jun-1994.)
A On       (B AB On)

Theoremonelssi 4112 A member of an ordinal number is a subset of it. (Contributed by NM, 11-Aug-1994.)
A On       (B ABA)

Theoremonelini 4113 An element of an ordinal number equals the intersection with it. (Contributed by NM, 11-Jun-1994.)
A On       (B AB = (BA))

Theoremoneluni 4114 An ordinal number equals its union with any element. (Contributed by NM, 13-Jun-1994.)
A On       (B A → (AB) = A)

Theoremonunisuci 4115 An ordinal number is equal to the union of its successor. (Contributed by NM, 12-Jun-1994.)
A On        suc A = A

2.4  IZF Set Theory - add the Axiom of Union

2.4.1  Introduce the Axiom of Union

Axiomax-un 4116* Axiom of Union. An axiom of Intuitionistic Zermelo-Fraenkel set theory. It states that a set y exists that includes the union of a given set x i.e. the collection of all members of the members of x. The variant axun2 4118 states that the union itself exists. A version with the standard abbreviation for union is uniex2 4119. A version using class notation is uniex 4120.

This is Axiom 3 of [Crosilla] p. "Axioms of CZF and IZF", except (a) unnecessary quantifiers are removed, (b) Crosilla has a biconditional rather than an implication (but the two are equivalent by bm1.3ii 3848), and (c) the order of the conjuncts is swapped (which is equivalent by ancom 253).

The union of a class df-uni 3551 should not be confused with the union of two classes df-un 2895. Their relationship is shown in unipr 3564. (Contributed by NM, 23-Dec-1993.)

yz(w(z w w x) → z y)

Theoremzfun 4117* Axiom of Union expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.)
xy(x(y x x z) → y x)

Theoremaxun2 4118* A variant of the Axiom of Union ax-un 4116. For any set x, there exists a set y whose members are exactly the members of the members of x i.e. the union of x. Axiom Union of [BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.)
yz(z yw(z w w x))

Theoremuniex2 4119* The Axiom of Union using the standard abbreviation for union. Given any set x, its union y exists. (Contributed by NM, 4-Jun-2006.)
y y = x

Theoremuniex 4120 The Axiom of Union in class notation. This says that if A is a set i.e. A V (see isset 2535), then the union of A is also a set. Same as Axiom 3 of [TakeutiZaring] p. 16. (Contributed by NM, 11-Aug-1993.)
A V        A V

Theoremuniexg 4121 The ZF Axiom of Union in class notation, in the form of a theorem instead of an inference. We use the antecedent A 𝑉 instead of A V to make the theorem more general and thus shorten some proofs; obviously the universal class constant V is one possible substitution for class variable 𝑉. (Contributed by NM, 25-Nov-1994.)
(A 𝑉 A V)

Theoremunex 4122 The union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 1-Jul-1994.)
A V    &   B V       (AB) V

Theoremunexb 4123 Existence of union is equivalent to existence of its components. (Contributed by NM, 11-Jun-1998.)
((A V B V) ↔ (AB) V)

Theoremunexg 4124 A union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 18-Sep-2006.)
((A 𝑉 B 𝑊) → (AB) V)

Theoremtpexg 4125 An unordered triple of classes exists. (Contributed by NM, 10-Apr-1994.)
((A 𝑈 B 𝑉 𝐶 𝑊) → {A, B, 𝐶} V)

Theoremunisn3 4126* Union of a singleton in the form of a restricted class abstraction. (Contributed by NM, 3-Jul-2008.)
(A B {x Bx = A} = A)

Theoremsnnex 4127* The class of all singletons is a proper class. (Contributed by NM, 10-Oct-2008.) (Proof shortened by Eric Schmidt, 7-Dec-2008.)
{xy x = {y}} ∉ V

Theoremopeluu 4128 Each member of an ordered pair belongs to the union of the union of a class to which the ordered pair belongs. Lemma 3D of [Enderton] p. 41. (Contributed by NM, 31-Mar-1995.) (Revised by Mario Carneiro, 27-Feb-2016.)
A V    &   B V       (⟨A, B 𝐶 → (A 𝐶 B 𝐶))

Theoremuniuni 4129* Expression for double union that moves union into a class builder. (Contributed by FL, 28-May-2007.)
A = {xy(x = y y A)}

Theoremeusv1 4130* Two ways to express single-valuedness of a class expression A(x). (Contributed by NM, 14-Oct-2010.)
(∃!yx y = Ayx y = A)

Theoremeusvnf 4131* Even if x is free in A, it is effectively bound when A(x) is single-valued. (Contributed by NM, 14-Oct-2010.) (Revised by Mario Carneiro, 14-Oct-2016.)
(∃!yx y = AxA)

Theoremeusvnfb 4132* Two ways to say that A(x) is a set expression that does not depend on x. (Contributed by Mario Carneiro, 18-Nov-2016.)
(∃!yx y = A ↔ (xA A V))

Theoremeusv2i 4133* Two ways to express single-valuedness of a class expression A(x). (Contributed by NM, 14-Oct-2010.) (Revised by Mario Carneiro, 18-Nov-2016.)
(∃!yx y = A∃!yx y = A)

Theoremeusv2nf 4134* Two ways to express single-valuedness of a class expression A(x). (Contributed by Mario Carneiro, 18-Nov-2016.)
A V       (∃!yx y = AxA)

Theoremeusv2 4135* Two ways to express single-valuedness of a class expression A(x). (Contributed by NM, 15-Oct-2010.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
A V       (∃!yx y = A∃!yx y = A)

Theoremreusv1 4136* Two ways to express single-valuedness of a class expression 𝐶(y). (Contributed by NM, 16-Dec-2012.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
(y B φ → (∃!x A y B (φx = 𝐶) ↔ x A y B (φx = 𝐶)))

Theoremreusv3i 4137* Two ways of expressing existential uniqueness via an indirect equality. (Contributed by NM, 23-Dec-2012.)
(y = z → (φψ))    &   (y = z𝐶 = 𝐷)       (x A y B (φx = 𝐶) → y B z B ((φ ψ) → 𝐶 = 𝐷))

Theoremreusv3 4138* Two ways to express single-valuedness of a class expression 𝐶(y). See reusv1 4136 for the connection to uniqueness. (Contributed by NM, 27-Dec-2012.)
(y = z → (φψ))    &   (y = z𝐶 = 𝐷)       (y B (φ 𝐶 A) → (y B z B ((φ ψ) → 𝐶 = 𝐷) ↔ x A y B (φx = 𝐶)))

Theoremalxfr 4139* Transfer universal quantification from a variable x to another variable y contained in expression A. (Contributed by NM, 18-Feb-2007.)
(x = A → (φψ))       ((y A B xy x = A) → (xφyψ))

Theoremralxfrd 4140* Transfer universal quantification from a variable x to another variable y contained in expression A. (Contributed by NM, 15-Aug-2014.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)
((φ y 𝐶) → A B)    &   ((φ x B) → y 𝐶 x = A)    &   ((φ x = A) → (ψχ))       (φ → (x B ψy 𝐶 χ))

Theoremrexxfrd 4141* Transfer universal quantification from a variable x to another variable y contained in expression A. (Contributed by FL, 10-Apr-2007.) (Revised by Mario Carneiro, 15-Aug-2014.)
((φ y 𝐶) → A B)    &   ((φ x B) → y 𝐶 x = A)    &   ((φ x = A) → (ψχ))       (φ → (x B ψy 𝐶 χ))

Theoremralxfr2d 4142* Transfer universal quantification from a variable x to another variable y contained in expression A. (Contributed by Mario Carneiro, 20-Aug-2014.)
((φ y 𝐶) → A 𝑉)    &   (φ → (x By 𝐶 x = A))    &   ((φ x = A) → (ψχ))       (φ → (x B ψy 𝐶 χ))

Theoremrexxfr2d 4143* Transfer universal quantification from a variable x to another variable y contained in expression A. (Contributed by Mario Carneiro, 20-Aug-2014.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)
((φ y 𝐶) → A 𝑉)    &   (φ → (x By 𝐶 x = A))    &   ((φ x = A) → (ψχ))       (φ → (x B ψy 𝐶 χ))

Theoremralxfr 4144* Transfer universal quantification from a variable x to another variable y contained in expression A. (Contributed by NM, 10-Jun-2005.) (Revised by Mario Carneiro, 15-Aug-2014.)
(y 𝐶A B)    &   (x By 𝐶 x = A)    &   (x = A → (φψ))       (x B φy 𝐶 ψ)

TheoremralxfrALT 4145* Transfer universal quantification from a variable x to another variable y contained in expression A. This proof does not use ralxfrd 4140. (Contributed by NM, 10-Jun-2005.) (Revised by Mario Carneiro, 15-Aug-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
(y 𝐶A B)    &   (x By 𝐶 x = A)    &   (x = A → (φψ))       (x B φy 𝐶 ψ)

Theoremrexxfr 4146* Transfer existence from a variable x to another variable y contained in expression A. (Contributed by NM, 10-Jun-2005.) (Revised by Mario Carneiro, 15-Aug-2014.)
(y 𝐶A B)    &   (x By 𝐶 x = A)    &   (x = A → (φψ))       (x B φy 𝐶 ψ)

Theoremrabxfrd 4147* Class builder membership after substituting an expression A (containing y) for x in the class expression χ. (Contributed by NM, 16-Jan-2012.)
yB    &   y𝐶    &   ((φ y 𝐷) → A 𝐷)    &   (x = A → (ψχ))    &   (y = BA = 𝐶)       ((φ B 𝐷) → (𝐶 {x 𝐷ψ} ↔ B {y 𝐷χ}))

Theoremrabxfr 4148* Class builder membership after substituting an expression A (containing y) for x in the class expression φ. (Contributed by NM, 10-Jun-2005.)
yB    &   y𝐶    &   (y 𝐷A 𝐷)    &   (x = A → (φψ))    &   (y = BA = 𝐶)       (B 𝐷 → (𝐶 {x 𝐷φ} ↔ B {y 𝐷ψ}))

Theoremreuhypd 4149* A theorem useful for eliminating restricted existential uniqueness hypotheses. (Contributed by NM, 16-Jan-2012.)
((φ x 𝐶) → B 𝐶)    &   ((φ x 𝐶 y 𝐶) → (x = Ay = B))       ((φ x 𝐶) → ∃!y 𝐶 x = A)

Theoremreuhyp 4150* A theorem useful for eliminating restricted existential uniqueness hypotheses. (Contributed by NM, 15-Nov-2004.)
(x 𝐶B 𝐶)    &   ((x 𝐶 y 𝐶) → (x = Ay = B))       (x 𝐶∃!y 𝐶 x = A)

Theoremuniexb 4151 The Axiom of Union and its converse. A class is a set iff its union is a set. (Contributed by NM, 11-Nov-2003.)
(A V ↔ A V)

Theorempwexb 4152 The Axiom of Power Sets and its converse. A class is a set iff its power class is a set. (Contributed by NM, 11-Nov-2003.)
(A V ↔ 𝒫 A V)

Theoremuniv 4153 The union of the universe is the universe. Exercise 4.12(c) of [Mendelson] p. 235. (Contributed by NM, 14-Sep-2003.)
V = V

Theoremeldifpw 4154 Membership in a power class difference. (Contributed by NM, 25-Mar-2007.)
𝐶 V       ((A 𝒫 B ¬ 𝐶B) → (A𝐶) (𝒫 (B𝐶) ∖ 𝒫 B))

Theoremop1stb 4155 Extract the first member of an ordered pair. Theorem 73 of [Suppes] p. 42. (Contributed by NM, 25-Nov-2003.)
A V    &   B V        A, B⟩ = A

Theoremop1stbg 4156 Extract the first member of an ordered pair. Theorem 73 of [Suppes] p. 42. (Contributed by Jim Kingdon, 17-Dec-2018.)
((A 𝑉 B 𝑊) → A, B⟩ = A)

Theoremiunpw 4157* An indexed union of a power class in terms of the power class of the union of its index. Part of Exercise 24(b) of [Enderton] p. 33. (Contributed by NM, 29-Nov-2003.)
A V       (x A x = A ↔ 𝒫 A = x A 𝒫 x)

2.4.2  Ordinals (continued)

Theoremordon 4158 The class of all ordinal numbers is ordinal. Proposition 7.12 of [TakeutiZaring] p. 38, but without using the Axiom of Regularity. (Contributed by NM, 17-May-1994.)
Ord On

Theoremssorduni 4159 The union of a class of ordinal numbers is ordinal. Proposition 7.19 of [TakeutiZaring] p. 40. (Contributed by NM, 30-May-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
(A ⊆ On → Ord A)

Theoremssonuni 4160 The union of a set of ordinal numbers is an ordinal number. Theorem 9 of [Suppes] p. 132. (Contributed by NM, 1-Nov-2003.)
(A 𝑉 → (A ⊆ On → A On))

Theoremssonunii 4161 The union of a set of ordinal numbers is an ordinal number. Corollary 7N(d) of [Enderton] p. 193. (Contributed by NM, 20-Sep-2003.)
A V       (A ⊆ On → A On)

Theoremonun2 4162 The union of two ordinal numbers is an ordinal number. (Contributed by Jim Kingdon, 25-Jul-2019.)
((A On B On) → (AB) On)

Theoremonun2i 4163 The union of two ordinal numbers is an ordinal number. (Contributed by NM, 13-Jun-1994.) (Constructive proof by Jim Kingdon, 25-Jul-2019.)
A On    &   B On       (AB) On

Theoremordsson 4164 Any ordinal class is a subclass of the class of ordinal numbers. Corollary 7.15 of [TakeutiZaring] p. 38. (Contributed by NM, 18-May-1994.)
(Ord AA ⊆ On)

Theoremonss 4165 An ordinal number is a subset of the class of ordinal numbers. (Contributed by NM, 5-Jun-1994.)
(A On → A ⊆ On)

Theoremonuni 4166 The union of an ordinal number is an ordinal number. (Contributed by NM, 29-Sep-2006.)
(A On → A On)

Theoremorduni 4167 The union of an ordinal class is ordinal. (Contributed by NM, 12-Sep-2003.)
(Ord A → Ord A)

Theorembm2.5ii 4168* Problem 2.5(ii) of [BellMachover] p. 471. (Contributed by NM, 20-Sep-2003.)
A V       (A ⊆ On → A = {x On ∣ y A yx})

Theoremsucexb 4169 A successor exists iff its class argument exists. (Contributed by NM, 22-Jun-1998.)
(A V ↔ suc A V)

Theoremsucexg 4170 The successor of a set is a set (generalization). (Contributed by NM, 5-Jun-1994.)
(A 𝑉 → suc A V)

Theoremsucex 4171 The successor of a set is a set. (Contributed by NM, 30-Aug-1993.)
A V       suc A V

Theoremordsucim 4172 The successor of an ordinal class is ordinal. (Contributed by Jim Kingdon, 8-Nov-2018.)
(Ord A → Ord suc A)

Theoremsuceloni 4173 The successor of an ordinal number is an ordinal number. Proposition 7.24 of [TakeutiZaring] p. 41. (Contributed by NM, 6-Jun-1994.)
(A On → suc A On)

Theoremordsucg 4174 The successor of an ordinal class is ordinal. (Contributed by Jim Kingdon, 20-Nov-2018.)
(A V → (Ord A ↔ Ord suc A))

Theoremsucelon 4175 The successor of an ordinal number is an ordinal number. (Contributed by NM, 9-Sep-2003.)
(A On ↔ suc A On)

Theoremordsucss 4176 The successor of an element of an ordinal class is a subset of it. (Contributed by NM, 21-Jun-1998.)
(Ord B → (A B → suc AB))

Theoremordelsuc 4177 A set belongs to an ordinal iff its successor is a subset of the ordinal. Exercise 8 of [TakeutiZaring] p. 42 and its converse. (Contributed by NM, 29-Nov-2003.)
((A 𝐶 Ord B) → (A B ↔ suc AB))

Theoremonsucmin 4178* The successor of an ordinal number is the smallest larger ordinal number. (Contributed by NM, 28-Nov-2003.)
(A On → suc A = {x On ∣ A x})

Theoremonsucelsucr 4179 Membership is inherited by predecessors. The converse, for all ordinals, implies excluded middle, as shown at onsucelsucexmid 4195. However, the converse does hold where B is a natural number, as seen at nnsucelsuc 5981. (Contributed by Jim Kingdon, 17-Jul-2019.)
(B On → (suc A suc BA B))

Theoremonsucsssucr 4180 The subclass relationship between two ordinals is inherited by their predecessors. The converse implies excluded middle, as shown at onsucsssucexmid 4192. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2019.)
((A On Ord B) → (suc A ⊆ suc BAB))

Theoremsucunielr 4181 Successor and union. The converse (where B is an ordinal) implies excluded middle, as seen at ordsucunielexmid 4196. (Contributed by Jim Kingdon, 2-Aug-2019.)
(suc A BA B)

Theoremunon 4182 The class of all ordinal numbers is its own union. Exercise 11 of [TakeutiZaring] p. 40. (Contributed by NM, 12-Nov-2003.)
On = On

Theoremonuniss2 4183* The union of the ordinal subsets of an ordinal number is that number. (Contributed by Jim Kingdon, 2-Aug-2019.)
(A On → {x On ∣ xA} = A)

Theoremlimon 4184 The class of ordinal numbers is a limit ordinal. (Contributed by NM, 24-Mar-1995.)
Lim On

Theoremordunisuc2r 4185* An ordinal which contains the successor of each of its members is equal to its union. (Contributed by Jim Kingdon, 14-Nov-2018.)
(Ord A → (x A suc x AA = A))

Theoremonssi 4186 An ordinal number is a subset of On. (Contributed by NM, 11-Aug-1994.)
A On       A ⊆ On

Theoremonsuci 4187 The successor of an ordinal number is an ordinal number. Corollary 7N(c) of [Enderton] p. 193. (Contributed by NM, 12-Jun-1994.)
A On       suc A On

Theoremordtriexmidlem 4188 Lemma for decidability and ordinals. The set {x {∅} ∣ φ} is a way of connecting statements about ordinals (such as trichotomy in ordtriexmid 4190 or weak linearity in ordsoexmid 4220) with a proposition φ. Our lemma states that it is an ordinal number. (Contributed by Jim Kingdon, 28-Jan-2019.)
{x {∅} ∣ φ} On

Theoremordtriexmidlem2 4189* Lemma for decidability and ordinals. The set {x {∅} ∣ φ} is a way of connecting statements about ordinals (such as trichotomy in ordtriexmid 4190 or weak linearity in ordsoexmid 4220) with a proposition φ. Our lemma helps connect that set to excluded middle. (Contributed by Jim Kingdon, 28-Jan-2019.)
({x {∅} ∣ φ} = ∅ → ¬ φ)

Theoremordtriexmid 4190* Ordinal trichotomy implies the law of the excluded middle (that is, decidability of an arbitrary proposition).

This theorem is stated in "Constructive ordinals", [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic".

(Contributed by Mario Carneiro and Jim Kingdon, 14-Nov-2018.)

x On y On (x y x = y y x)       (φ ¬ φ)

Theoremordtri2orexmid 4191* Ordinal trichotomy implies excluded middle. (Contributed by Jim Kingdon, 31-Jul-2019.)
x On y On (x y yx)       (φ ¬ φ)

Theoremonsucsssucexmid 4192* The converse of onsucsssucr 4180 implies excluded middle. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2019.)
x On y On (xy → suc x ⊆ suc y)       (φ ¬ φ)

Theoremonsucelsucexmidlem1 4193* Lemma for onsucelsucexmid 4195. (Contributed by Jim Kingdon, 2-Aug-2019.)
{x {∅, {∅}} ∣ (x = ∅ φ)}

Theoremonsucelsucexmidlem 4194* Lemma for onsucelsucexmid 4195. The set {x {∅, {∅}} ∣ (x = ∅ φ)} appears as A in the proof of Theorem 1.3 in [Bauer] p. 483 (see acexmidlema 5423), and similar sets also appear in other proofs that various propositions imply excluded middle, for example in ordtriexmidlem 4188. (Contributed by Jim Kingdon, 2-Aug-2019.)
{x {∅, {∅}} ∣ (x = ∅ φ)} On

Theoremonsucelsucexmid 4195* The converse of onsucelsucr 4179 implies excluded middle. On the other hand, if y is constrained to be a natural number, instead of an arbitrary ordinal, then the converse of onsucelsucr 4179 does hold, as seen at nnsucelsuc 5981. (Contributed by Jim Kingdon, 2-Aug-2019.)
x On y On (x y → suc x suc y)       (φ ¬ φ)

Theoremordsucunielexmid 4196* The converse of sucunielr 4181 (where B is an ordinal) implies excluded middle. (Contributed by Jim Kingdon, 2-Aug-2019.)
x On y On (x y → suc x y)       (φ ¬ φ)

2.5  IZF Set Theory - add the Axiom of Set Induction

2.5.1  The ZF Axiom of Foundation would imply Excluded Middle

Theoremregexmidlemm 4197* Lemma for regexmid 4199. A is inhabited. (Contributed by Jim Kingdon, 3-Sep-2019.)
A = {x {∅, {∅}} ∣ (x = {∅} (x = ∅ φ))}       y y A

Theoremregexmidlem1 4198* Lemma for regexmid 4199. If A has a minimal element, excluded middle follows. (Contributed by Jim Kingdon, 3-Sep-2019.)
A = {x {∅, {∅}} ∣ (x = {∅} (x = ∅ φ))}       (y(y A z(z y → ¬ z A)) → (φ ¬ φ))

Theoremregexmid 4199* The axiom of foundation implies excluded middle.

By foundation (or regularity), we mean the principle that every inhabited set has an element which is minimal (when arranged by ). The statement of foundation here is taken from Metamath Proof Explorer's ax-reg, and is identical (modulo one unnecessary quantifier) to the statement of foundation in Theorem "Foundation implies instances of EM" of [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic".

For this reason, IZF does not adopt foundation as an axiom and instead replaces it with ax-setind 4200. (Contributed by Jim Kingdon, 3-Sep-2019.)

(y y xy(y x z(z y → ¬ z x)))       (φ ¬ φ)

2.5.2  Introduce the Axiom of Set Induction

Axiomax-setind 4200* Axiom of -Induction (also known as set induction). An axiom of Intuitionistic Zermelo-Fraenkel set theory. Axiom 9 of [Crosilla] p. "Axioms of CZF and IZF". This replaces the Axiom of Foundation (also called Regularity) from Zermelo-Fraenkel set theory. (Contributed by Jim Kingdon, 19-Oct-2018.)
(𝑎(y 𝑎 [y / 𝑎]φφ) → 𝑎φ)

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7354
 Copyright terms: Public domain < Previous  Next >