Home | Intuitionistic Logic Explorer Theorem 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 |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | eqelsuc 4101 | A set belongs to the successor of an equal set. (Contributed by NM, 18-Aug-1994.) |
⊢ A ∈ V ⇒ ⊢ (A = B → A ∈ suc B) | ||
Theorem | iunsuc 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 = A → B = 𝐶) ⇒ ⊢ ∪ x ∈ suc AB = (∪ x ∈ A B ∪ 𝐶) | ||
Theorem | suctrALT 4103 | The successor of a transtive class is transitive. (Contributed by Alan Sare, 11-Apr-2009.) |
⊢ (Tr A → Tr suc A) | ||
Theorem | suctr 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) | ||
Theorem | trsuc 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) | ||
Theorem | trsucss 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 A → B ⊆ A)) | ||
Theorem | sucssel 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 A ⊆ B → A ∈ B)) | ||
Theorem | orduniss 4108 | An ordinal class includes its union. (Contributed by NM, 13-Sep-2003.) |
⊢ (Ord A → ∪ A ⊆ A) | ||
Theorem | onordi 4109 | An ordinal number is an ordinal class. (Contributed by NM, 11-Jun-1994.) |
⊢ A ∈ On ⇒ ⊢ Ord A | ||
Theorem | ontrci 4110 | An ordinal number is a transitive class. (Contributed by NM, 11-Jun-1994.) |
⊢ A ∈ On ⇒ ⊢ Tr A | ||
Theorem | oneli 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 ∈ A → B ∈ On) | ||
Theorem | onelssi 4112 | A member of an ordinal number is a subset of it. (Contributed by NM, 11-Aug-1994.) |
⊢ A ∈ On ⇒ ⊢ (B ∈ A → B ⊆ A) | ||
Theorem | onelini 4113 | An element of an ordinal number equals the intersection with it. (Contributed by NM, 11-Jun-1994.) |
⊢ A ∈ On ⇒ ⊢ (B ∈ A → B = (B ∩ A)) | ||
Theorem | oneluni 4114 | An ordinal number equals its union with any element. (Contributed by NM, 13-Jun-1994.) |
⊢ A ∈ On ⇒ ⊢ (B ∈ A → (A ∪ B) = A) | ||
Theorem | onunisuci 4115 | An ordinal number is equal to the union of its successor. (Contributed by NM, 12-Jun-1994.) |
⊢ A ∈ On ⇒ ⊢ ∪ suc A = A | ||
Axiom | ax-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.) |
⊢ ∃y∀z(∃w(z ∈ w ∧ w ∈ x) → z ∈ y) | ||
Theorem | zfun 4117* | Axiom of Union expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.) |
⊢ ∃x∀y(∃x(y ∈ x ∧ x ∈ z) → y ∈ x) | ||
Theorem | axun2 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.) |
⊢ ∃y∀z(z ∈ y ↔ ∃w(z ∈ w ∧ w ∈ x)) | ||
Theorem | uniex2 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 | ||
Theorem | uniex 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 | ||
Theorem | uniexg 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) | ||
Theorem | unex 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 ⇒ ⊢ (A ∪ B) ∈ V | ||
Theorem | unexb 4123 | Existence of union is equivalent to existence of its components. (Contributed by NM, 11-Jun-1998.) |
⊢ ((A ∈ V ∧ B ∈ V) ↔ (A ∪ B) ∈ V) | ||
Theorem | unexg 4124 | A union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 18-Sep-2006.) |
⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → (A ∪ B) ∈ V) | ||
Theorem | tpexg 4125 | An unordered triple of classes exists. (Contributed by NM, 10-Apr-1994.) |
⊢ ((A ∈ 𝑈 ∧ B ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → {A, B, 𝐶} ∈ V) | ||
Theorem | unisn3 4126* | Union of a singleton in the form of a restricted class abstraction. (Contributed by NM, 3-Jul-2008.) |
⊢ (A ∈ B → ∪ {x ∈ B ∣ x = A} = A) | ||
Theorem | snnex 4127* | The class of all singletons is a proper class. (Contributed by NM, 10-Oct-2008.) (Proof shortened by Eric Schmidt, 7-Dec-2008.) |
⊢ {x ∣ ∃y x = {y}} ∉ V | ||
Theorem | opeluu 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 ∈ ∪ ∪ 𝐶)) | ||
Theorem | uniuni 4129* | Expression for double union that moves union into a class builder. (Contributed by FL, 28-May-2007.) |
⊢ ∪ ∪ A = ∪ {x ∣ ∃y(x = ∪ y ∧ y ∈ A)} | ||
Theorem | eusv1 4130* | Two ways to express single-valuedness of a class expression A(x). (Contributed by NM, 14-Oct-2010.) |
⊢ (∃!y∀x y = A ↔ ∃y∀x y = A) | ||
Theorem | eusvnf 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.) |
⊢ (∃!y∀x y = A → ℲxA) | ||
Theorem | eusvnfb 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.) |
⊢ (∃!y∀x y = A ↔ (ℲxA ∧ A ∈ V)) | ||
Theorem | eusv2i 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.) |
⊢ (∃!y∀x y = A → ∃!y∃x y = A) | ||
Theorem | eusv2nf 4134* | Two ways to express single-valuedness of a class expression A(x). (Contributed by Mario Carneiro, 18-Nov-2016.) |
⊢ A ∈ V ⇒ ⊢ (∃!y∃x y = A ↔ ℲxA) | ||
Theorem | eusv2 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 ⇒ ⊢ (∃!y∃x y = A ↔ ∃!y∀x y = A) | ||
Theorem | reusv1 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 = 𝐶))) | ||
Theorem | reusv3i 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 ((φ ∧ ψ) → 𝐶 = 𝐷)) | ||
Theorem | reusv3 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 = 𝐶))) | ||
Theorem | alxfr 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 ∧ ∀x∃y x = A) → (∀xφ ↔ ∀yψ)) | ||
Theorem | ralxfrd 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 ∈ 𝐶 χ)) | ||
Theorem | rexxfrd 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 ∈ 𝐶 χ)) | ||
Theorem | ralxfr2d 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 ∈ B ↔ ∃y ∈ 𝐶 x = A)) & ⊢ ((φ ∧ x = A) → (ψ ↔ χ)) ⇒ ⊢ (φ → (∀x ∈ B ψ ↔ ∀y ∈ 𝐶 χ)) | ||
Theorem | rexxfr2d 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 ∈ B ↔ ∃y ∈ 𝐶 x = A)) & ⊢ ((φ ∧ x = A) → (ψ ↔ χ)) ⇒ ⊢ (φ → (∃x ∈ B ψ ↔ ∃y ∈ 𝐶 χ)) | ||
Theorem | ralxfr 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 ∈ B → ∃y ∈ 𝐶 x = A) & ⊢ (x = A → (φ ↔ ψ)) ⇒ ⊢ (∀x ∈ B φ ↔ ∀y ∈ 𝐶 ψ) | ||
Theorem | ralxfrALT 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 ∈ B → ∃y ∈ 𝐶 x = A) & ⊢ (x = A → (φ ↔ ψ)) ⇒ ⊢ (∀x ∈ B φ ↔ ∀y ∈ 𝐶 ψ) | ||
Theorem | rexxfr 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 ∈ B → ∃y ∈ 𝐶 x = A) & ⊢ (x = A → (φ ↔ ψ)) ⇒ ⊢ (∃x ∈ B φ ↔ ∃y ∈ 𝐶 ψ) | ||
Theorem | rabxfrd 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 = B → A = 𝐶) ⇒ ⊢ ((φ ∧ B ∈ 𝐷) → (𝐶 ∈ {x ∈ 𝐷 ∣ ψ} ↔ B ∈ {y ∈ 𝐷 ∣ χ})) | ||
Theorem | rabxfr 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 = B → A = 𝐶) ⇒ ⊢ (B ∈ 𝐷 → (𝐶 ∈ {x ∈ 𝐷 ∣ φ} ↔ B ∈ {y ∈ 𝐷 ∣ ψ})) | ||
Theorem | reuhypd 4149* | A theorem useful for eliminating restricted existential uniqueness hypotheses. (Contributed by NM, 16-Jan-2012.) |
⊢ ((φ ∧ x ∈ 𝐶) → B ∈ 𝐶) & ⊢ ((φ ∧ x ∈ 𝐶 ∧ y ∈ 𝐶) → (x = A ↔ y = B)) ⇒ ⊢ ((φ ∧ x ∈ 𝐶) → ∃!y ∈ 𝐶 x = A) | ||
Theorem | reuhyp 4150* | A theorem useful for eliminating restricted existential uniqueness hypotheses. (Contributed by NM, 15-Nov-2004.) |
⊢ (x ∈ 𝐶 → B ∈ 𝐶) & ⊢ ((x ∈ 𝐶 ∧ y ∈ 𝐶) → (x = A ↔ y = B)) ⇒ ⊢ (x ∈ 𝐶 → ∃!y ∈ 𝐶 x = A) | ||
Theorem | uniexb 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) | ||
Theorem | pwexb 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) | ||
Theorem | univ 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 | ||
Theorem | eldifpw 4154 | Membership in a power class difference. (Contributed by NM, 25-Mar-2007.) |
⊢ 𝐶 ∈ V ⇒ ⊢ ((A ∈ 𝒫 B ∧ ¬ 𝐶 ⊆ B) → (A ∪ 𝐶) ∈ (𝒫 (B ∪ 𝐶) ∖ 𝒫 B)) | ||
Theorem | op1stb 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 | ||
Theorem | op1stbg 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) | ||
Theorem | iunpw 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) | ||
Theorem | ordon 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 | ||
Theorem | ssorduni 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) | ||
Theorem | ssonuni 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)) | ||
Theorem | ssonunii 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) | ||
Theorem | onun2 4162 | The union of two ordinal numbers is an ordinal number. (Contributed by Jim Kingdon, 25-Jul-2019.) |
⊢ ((A ∈ On ∧ B ∈ On) → (A ∪ B) ∈ On) | ||
Theorem | onun2i 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 ⇒ ⊢ (A ∪ B) ∈ On | ||
Theorem | ordsson 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 A → A ⊆ On) | ||
Theorem | onss 4165 | An ordinal number is a subset of the class of ordinal numbers. (Contributed by NM, 5-Jun-1994.) |
⊢ (A ∈ On → A ⊆ On) | ||
Theorem | onuni 4166 | The union of an ordinal number is an ordinal number. (Contributed by NM, 29-Sep-2006.) |
⊢ (A ∈ On → ∪ A ∈ On) | ||
Theorem | orduni 4167 | The union of an ordinal class is ordinal. (Contributed by NM, 12-Sep-2003.) |
⊢ (Ord A → Ord ∪ A) | ||
Theorem | bm2.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 y ⊆ x}) | ||
Theorem | sucexb 4169 | A successor exists iff its class argument exists. (Contributed by NM, 22-Jun-1998.) |
⊢ (A ∈ V ↔ suc A ∈ V) | ||
Theorem | sucexg 4170 | The successor of a set is a set (generalization). (Contributed by NM, 5-Jun-1994.) |
⊢ (A ∈ 𝑉 → suc A ∈ V) | ||
Theorem | sucex 4171 | The successor of a set is a set. (Contributed by NM, 30-Aug-1993.) |
⊢ A ∈ V ⇒ ⊢ suc A ∈ V | ||
Theorem | ordsucim 4172 | The successor of an ordinal class is ordinal. (Contributed by Jim Kingdon, 8-Nov-2018.) |
⊢ (Ord A → Ord suc A) | ||
Theorem | suceloni 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) | ||
Theorem | ordsucg 4174 | The successor of an ordinal class is ordinal. (Contributed by Jim Kingdon, 20-Nov-2018.) |
⊢ (A ∈ V → (Ord A ↔ Ord suc A)) | ||
Theorem | sucelon 4175 | The successor of an ordinal number is an ordinal number. (Contributed by NM, 9-Sep-2003.) |
⊢ (A ∈ On ↔ suc A ∈ On) | ||
Theorem | ordsucss 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 A ⊆ B)) | ||
Theorem | ordelsuc 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 A ⊆ B)) | ||
Theorem | onsucmin 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}) | ||
Theorem | onsucelsucr 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 B → A ∈ B)) | ||
Theorem | onsucsssucr 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 B → A ⊆ B)) | ||
Theorem | sucunielr 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 ∈ B → A ∈ ∪ B) | ||
Theorem | unon 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 | ||
Theorem | onuniss2 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 ∣ x ⊆ A} = A) | ||
Theorem | limon 4184 | The class of ordinal numbers is a limit ordinal. (Contributed by NM, 24-Mar-1995.) |
⊢ Lim On | ||
Theorem | ordunisuc2r 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 ∈ A → A = ∪ A)) | ||
Theorem | onssi 4186 | An ordinal number is a subset of On. (Contributed by NM, 11-Aug-1994.) |
⊢ A ∈ On ⇒ ⊢ A ⊆ On | ||
Theorem | onsuci 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 | ||
Theorem | ordtriexmidlem 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 | ||
Theorem | ordtriexmidlem2 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 ∈ {∅} ∣ φ} = ∅ → ¬ φ) | ||
Theorem | ordtriexmid 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) ⇒ ⊢ (φ ∨ ¬ φ) | ||
Theorem | ordtri2orexmid 4191* | Ordinal trichotomy implies excluded middle. (Contributed by Jim Kingdon, 31-Jul-2019.) |
⊢ ∀x ∈ On ∀y ∈ On (x ∈ y ∨ y ⊆ x) ⇒ ⊢ (φ ∨ ¬ φ) | ||
Theorem | onsucsssucexmid 4192* | The converse of onsucsssucr 4180 implies excluded middle. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2019.) |
⊢ ∀x ∈ On ∀y ∈ On (x ⊆ y → suc x ⊆ suc y) ⇒ ⊢ (φ ∨ ¬ φ) | ||
Theorem | onsucelsucexmidlem1 4193* | Lemma for onsucelsucexmid 4195. (Contributed by Jim Kingdon, 2-Aug-2019.) |
⊢ ∅ ∈ {x ∈ {∅, {∅}} ∣ (x = ∅ ∨ φ)} | ||
Theorem | onsucelsucexmidlem 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 | ||
Theorem | onsucelsucexmid 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) ⇒ ⊢ (φ ∨ ¬ φ) | ||
Theorem | ordsucunielexmid 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) ⇒ ⊢ (φ ∨ ¬ φ) | ||
Theorem | regexmidlemm 4197* | Lemma for regexmid 4199. A is inhabited. (Contributed by Jim Kingdon, 3-Sep-2019.) |
⊢ A = {x ∈ {∅, {∅}} ∣ (x = {∅} ∨ (x = ∅ ∧ φ))} ⇒ ⊢ ∃y y ∈ A | ||
Theorem | regexmidlem1 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)) → (φ ∨ ¬ φ)) | ||
Theorem | regexmid 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 ∈ x → ∃y(y ∈ x ∧ ∀z(z ∈ y → ¬ z ∈ x))) ⇒ ⊢ (φ ∨ ¬ φ) | ||
Axiom | ax-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 / 𝑎]φ → φ) → ∀𝑎φ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |