Home | Intuitionistic Logic Explorer Theorem List (p. 45 of 139) | < 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 | onelssi 4401 | A member of an ordinal number is a subset of it. (Contributed by NM, 11-Aug-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴) | ||
Theorem | onelini 4402 | An element of an ordinal number equals the intersection with it. (Contributed by NM, 11-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ (𝐵 ∈ 𝐴 → 𝐵 = (𝐵 ∩ 𝐴)) | ||
Theorem | oneluni 4403 | An ordinal number equals its union with any element. (Contributed by NM, 13-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ (𝐵 ∈ 𝐴 → (𝐴 ∪ 𝐵) = 𝐴) | ||
Theorem | onunisuci 4404 | An ordinal number is equal to the union of its successor. (Contributed by NM, 12-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ ∪ suc 𝐴 = 𝐴 | ||
Axiom | ax-un 4405* |
Axiom of Union. An axiom of Intuitionistic Zermelo-Fraenkel set theory.
It states that a set 𝑦 exists that includes the union of a
given set
𝑥 i.e. the collection of all members of
the members of 𝑥. The
variant axun2 4407 states that the union itself exists. A
version with the
standard abbreviation for union is uniex2 4408. A version using class
notation is uniex 4409.
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 4097), and (c) the order of the conjuncts is swapped (which is equivalent by ancom 264). The union of a class df-uni 3784 should not be confused with the union of two classes df-un 3115. Their relationship is shown in unipr 3797. (Contributed by NM, 23-Dec-1993.) |
⊢ ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) | ||
Theorem | zfun 4406* | Axiom of Union expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.) |
⊢ ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥) | ||
Theorem | axun2 4407* | A variant of the Axiom of Union ax-un 4405. For any set 𝑥, there exists a set 𝑦 whose members are exactly the members of the members of 𝑥 i.e. the union of 𝑥. Axiom Union of [BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.) |
⊢ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) | ||
Theorem | uniex2 4408* | The Axiom of Union using the standard abbreviation for union. Given any set 𝑥, its union 𝑦 exists. (Contributed by NM, 4-Jun-2006.) |
⊢ ∃𝑦 𝑦 = ∪ 𝑥 | ||
Theorem | uniex 4409 | The Axiom of Union in class notation. This says that if 𝐴 is a set i.e. 𝐴 ∈ V (see isset 2727), then the union of 𝐴 is also a set. Same as Axiom 3 of [TakeutiZaring] p. 16. (Contributed by NM, 11-Aug-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ∪ 𝐴 ∈ V | ||
Theorem | vuniex 4410 | The union of a setvar is a set. (Contributed by BJ, 3-May-2021.) |
⊢ ∪ 𝑥 ∈ V | ||
Theorem | uniexg 4411 | The ZF Axiom of Union in class notation, in the form of a theorem instead of an inference. We use the antecedent 𝐴 ∈ 𝑉 instead of 𝐴 ∈ 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.) |
⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) | ||
Theorem | uniexd 4412 | Deduction version of the ZF Axiom of Union in class notation. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∪ 𝐴 ∈ V) | ||
Theorem | unex 4413 | The union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 1-Jul-1994.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∪ 𝐵) ∈ V | ||
Theorem | unexb 4414 | Existence of union is equivalent to existence of its components. (Contributed by NM, 11-Jun-1998.) |
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴 ∪ 𝐵) ∈ V) | ||
Theorem | unexg 4415 | A union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 18-Sep-2006.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) | ||
Theorem | tpexg 4416 | An unordered triple of classes exists. (Contributed by NM, 10-Apr-1994.) |
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → {𝐴, 𝐵, 𝐶} ∈ V) | ||
Theorem | unisn3 4417* | Union of a singleton in the form of a restricted class abstraction. (Contributed by NM, 3-Jul-2008.) |
⊢ (𝐴 ∈ 𝐵 → ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 = 𝐴} = 𝐴) | ||
Theorem | abnexg 4418* | Sufficient condition for a class abstraction to be a proper class. The class 𝐹 can be thought of as an expression in 𝑥 and the abstraction appearing in the statement as the class of values 𝐹 as 𝑥 varies through 𝐴. Assuming the antecedents, if that class is a set, then so is the "domain" 𝐴. The converse holds without antecedent, see abrexexg 6078. Note that the second antecedent ∀𝑥 ∈ 𝐴𝑥 ∈ 𝐹 cannot be translated to 𝐴 ⊆ 𝐹 since 𝐹 may depend on 𝑥. In applications, one may take 𝐹 = {𝑥} or 𝐹 = 𝒫 𝑥 (see snnex 4420 and pwnex 4421 respectively, proved from abnex 4419, which is a consequence of abnexg 4418 with 𝐴 = V). (Contributed by BJ, 2-Dec-2021.) |
⊢ (∀𝑥 ∈ 𝐴 (𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹) → ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐹} ∈ 𝑊 → 𝐴 ∈ V)) | ||
Theorem | abnex 4419* | Sufficient condition for a class abstraction to be a proper class. Lemma for snnex 4420 and pwnex 4421. See the comment of abnexg 4418. (Contributed by BJ, 2-May-2021.) |
⊢ (∀𝑥(𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹) → ¬ {𝑦 ∣ ∃𝑥 𝑦 = 𝐹} ∈ V) | ||
Theorem | snnex 4420* | The class of all singletons is a proper class. (Contributed by NM, 10-Oct-2008.) (Proof shortened by Eric Schmidt, 7-Dec-2008.) |
⊢ {𝑥 ∣ ∃𝑦 𝑥 = {𝑦}} ∉ V | ||
Theorem | pwnex 4421* | The class of all power sets is a proper class. See also snnex 4420. (Contributed by BJ, 2-May-2021.) |
⊢ {𝑥 ∣ ∃𝑦 𝑥 = 𝒫 𝑦} ∉ V | ||
Theorem | opeluu 4422 | 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.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ 𝐶 → (𝐴 ∈ ∪ ∪ 𝐶 ∧ 𝐵 ∈ ∪ ∪ 𝐶)) | ||
Theorem | uniuni 4423* | Expression for double union that moves union into a class builder. (Contributed by FL, 28-May-2007.) |
⊢ ∪ ∪ 𝐴 = ∪ {𝑥 ∣ ∃𝑦(𝑥 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴)} | ||
Theorem | eusv1 4424* | Two ways to express single-valuedness of a class expression 𝐴(𝑥). (Contributed by NM, 14-Oct-2010.) |
⊢ (∃!𝑦∀𝑥 𝑦 = 𝐴 ↔ ∃𝑦∀𝑥 𝑦 = 𝐴) | ||
Theorem | eusvnf 4425* | Even if 𝑥 is free in 𝐴, it is effectively bound when 𝐴(𝑥) is single-valued. (Contributed by NM, 14-Oct-2010.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ (∃!𝑦∀𝑥 𝑦 = 𝐴 → Ⅎ𝑥𝐴) | ||
Theorem | eusvnfb 4426* | Two ways to say that 𝐴(𝑥) is a set expression that does not depend on 𝑥. (Contributed by Mario Carneiro, 18-Nov-2016.) |
⊢ (∃!𝑦∀𝑥 𝑦 = 𝐴 ↔ (Ⅎ𝑥𝐴 ∧ 𝐴 ∈ V)) | ||
Theorem | eusv2i 4427* | Two ways to express single-valuedness of a class expression 𝐴(𝑥). (Contributed by NM, 14-Oct-2010.) (Revised by Mario Carneiro, 18-Nov-2016.) |
⊢ (∃!𝑦∀𝑥 𝑦 = 𝐴 → ∃!𝑦∃𝑥 𝑦 = 𝐴) | ||
Theorem | eusv2nf 4428* | Two ways to express single-valuedness of a class expression 𝐴(𝑥). (Contributed by Mario Carneiro, 18-Nov-2016.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (∃!𝑦∃𝑥 𝑦 = 𝐴 ↔ Ⅎ𝑥𝐴) | ||
Theorem | eusv2 4429* | Two ways to express single-valuedness of a class expression 𝐴(𝑥). (Contributed by NM, 15-Oct-2010.) (Proof shortened by Mario Carneiro, 18-Nov-2016.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (∃!𝑦∃𝑥 𝑦 = 𝐴 ↔ ∃!𝑦∀𝑥 𝑦 = 𝐴) | ||
Theorem | reusv1 4430* | Two ways to express single-valuedness of a class expression 𝐶(𝑦). (Contributed by NM, 16-Dec-2012.) (Proof shortened by Mario Carneiro, 18-Nov-2016.) |
⊢ (∃𝑦 ∈ 𝐵 𝜑 → (∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶) ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶))) | ||
Theorem | reusv3i 4431* | Two ways of expressing existential uniqueness via an indirect equality. (Contributed by NM, 23-Dec-2012.) |
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝑧 → 𝐶 = 𝐷) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝜑 ∧ 𝜓) → 𝐶 = 𝐷)) | ||
Theorem | reusv3 4432* | Two ways to express single-valuedness of a class expression 𝐶(𝑦). See reusv1 4430 for the connection to uniqueness. (Contributed by NM, 27-Dec-2012.) |
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝑧 → 𝐶 = 𝐷) ⇒ ⊢ (∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝐶 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝜑 ∧ 𝜓) → 𝐶 = 𝐷) ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶))) | ||
Theorem | alxfr 4433* | Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by NM, 18-Feb-2007.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((∀𝑦 𝐴 ∈ 𝐵 ∧ ∀𝑥∃𝑦 𝑥 = 𝐴) → (∀𝑥𝜑 ↔ ∀𝑦𝜓)) | ||
Theorem | ralxfrd 4434* | Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by NM, 15-Aug-2014.) (Proof shortened by Mario Carneiro, 19-Nov-2016.) |
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐶 𝜒)) | ||
Theorem | rexxfrd 4435* | Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by FL, 10-Apr-2007.) (Revised by Mario Carneiro, 15-Aug-2014.) |
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐶 𝜒)) | ||
Theorem | ralxfr2d 4436* | Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by Mario Carneiro, 20-Aug-2014.) |
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐶 𝑥 = 𝐴)) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐶 𝜒)) | ||
Theorem | rexxfr2d 4437* | Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by Mario Carneiro, 20-Aug-2014.) (Proof shortened by Mario Carneiro, 19-Nov-2016.) |
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐶 𝑥 = 𝐴)) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐶 𝜒)) | ||
Theorem | ralxfr 4438* | Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by NM, 10-Jun-2005.) (Revised by Mario Carneiro, 15-Aug-2014.) |
⊢ (𝑦 ∈ 𝐶 → 𝐴 ∈ 𝐵) & ⊢ (𝑥 ∈ 𝐵 → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐶 𝜓) | ||
Theorem | ralxfrALT 4439* | Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. This proof does not use ralxfrd 4434. (Contributed by NM, 10-Jun-2005.) (Revised by Mario Carneiro, 15-Aug-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑦 ∈ 𝐶 → 𝐴 ∈ 𝐵) & ⊢ (𝑥 ∈ 𝐵 → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐶 𝜓) | ||
Theorem | rexxfr 4440* | Transfer existence from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by NM, 10-Jun-2005.) (Revised by Mario Carneiro, 15-Aug-2014.) |
⊢ (𝑦 ∈ 𝐶 → 𝐴 ∈ 𝐵) & ⊢ (𝑥 ∈ 𝐵 → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐶 𝜓) | ||
Theorem | rabxfrd 4441* | Class builder membership after substituting an expression 𝐴 (containing 𝑦) for 𝑥 in the class expression 𝜒. (Contributed by NM, 16-Jan-2012.) |
⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑦𝐶 & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝐴 ∈ 𝐷) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → 𝐴 = 𝐶) ⇒ ⊢ ((𝜑 ∧ 𝐵 ∈ 𝐷) → (𝐶 ∈ {𝑥 ∈ 𝐷 ∣ 𝜓} ↔ 𝐵 ∈ {𝑦 ∈ 𝐷 ∣ 𝜒})) | ||
Theorem | rabxfr 4442* | Class builder membership after substituting an expression 𝐴 (containing 𝑦) for 𝑥 in the class expression 𝜑. (Contributed by NM, 10-Jun-2005.) |
⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑦𝐶 & ⊢ (𝑦 ∈ 𝐷 → 𝐴 ∈ 𝐷) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → 𝐴 = 𝐶) ⇒ ⊢ (𝐵 ∈ 𝐷 → (𝐶 ∈ {𝑥 ∈ 𝐷 ∣ 𝜑} ↔ 𝐵 ∈ {𝑦 ∈ 𝐷 ∣ 𝜓})) | ||
Theorem | reuhypd 4443* | A theorem useful for eliminating restricted existential uniqueness hypotheses. (Contributed by NM, 16-Jan-2012.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐵 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶) → (𝑥 = 𝐴 ↔ 𝑦 = 𝐵)) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∃!𝑦 ∈ 𝐶 𝑥 = 𝐴) | ||
Theorem | reuhyp 4444* | A theorem useful for eliminating restricted existential uniqueness hypotheses. (Contributed by NM, 15-Nov-2004.) |
⊢ (𝑥 ∈ 𝐶 → 𝐵 ∈ 𝐶) & ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶) → (𝑥 = 𝐴 ↔ 𝑦 = 𝐵)) ⇒ ⊢ (𝑥 ∈ 𝐶 → ∃!𝑦 ∈ 𝐶 𝑥 = 𝐴) | ||
Theorem | uniexb 4445 | The Axiom of Union and its converse. A class is a set iff its union is a set. (Contributed by NM, 11-Nov-2003.) |
⊢ (𝐴 ∈ V ↔ ∪ 𝐴 ∈ V) | ||
Theorem | pwexb 4446 | 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.) |
⊢ (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V) | ||
Theorem | elpwpwel 4447 | A class belongs to a double power class if and only if its union belongs to the power class. (Contributed by BJ, 22-Jan-2023.) |
⊢ (𝐴 ∈ 𝒫 𝒫 𝐵 ↔ ∪ 𝐴 ∈ 𝒫 𝐵) | ||
Theorem | univ 4448 | 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 4449 | Membership in a power class difference. (Contributed by NM, 25-Mar-2007.) |
⊢ 𝐶 ∈ V ⇒ ⊢ ((𝐴 ∈ 𝒫 𝐵 ∧ ¬ 𝐶 ⊆ 𝐵) → (𝐴 ∪ 𝐶) ∈ (𝒫 (𝐵 ∪ 𝐶) ∖ 𝒫 𝐵)) | ||
Theorem | op1stb 4450 | Extract the first member of an ordered pair. Theorem 73 of [Suppes] p. 42. (Contributed by NM, 25-Nov-2003.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∩ ∩ 〈𝐴, 𝐵〉 = 𝐴 | ||
Theorem | op1stbg 4451 | Extract the first member of an ordered pair. Theorem 73 of [Suppes] p. 42. (Contributed by Jim Kingdon, 17-Dec-2018.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∩ ∩ 〈𝐴, 𝐵〉 = 𝐴) | ||
Theorem | iunpw 4452* | 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.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝑥 = ∪ 𝐴 ↔ 𝒫 ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝒫 𝑥) | ||
Theorem | ifelpwung 4453 | Existence of a conditional class, quantitative version (closed form). (Contributed by BJ, 15-Aug-2024.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → if(𝜑, 𝐴, 𝐵) ∈ 𝒫 (𝐴 ∪ 𝐵)) | ||
Theorem | ifelpwund 4454 | Existence of a conditional class, quantitative version (deduction form). (Contributed by BJ, 15-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) ∈ 𝒫 (𝐴 ∪ 𝐵)) | ||
Theorem | ifelpwun 4455 | Existence of a conditional class, quantitative version (inference form). (Contributed by BJ, 15-Aug-2024.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ if(𝜑, 𝐴, 𝐵) ∈ 𝒫 (𝐴 ∪ 𝐵) | ||
Theorem | ifexd 4456 | Existence of a conditional class (deduction form). (Contributed by BJ, 15-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) ∈ V) | ||
Theorem | ordon 4457 | 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 4458 | 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.) |
⊢ (𝐴 ⊆ On → Ord ∪ 𝐴) | ||
Theorem | ssonuni 4459 | The union of a set of ordinal numbers is an ordinal number. Theorem 9 of [Suppes] p. 132. (Contributed by NM, 1-Nov-2003.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ⊆ On → ∪ 𝐴 ∈ On)) | ||
Theorem | ssonunii 4460 | 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.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ⊆ On → ∪ 𝐴 ∈ On) | ||
Theorem | onun2 4461 | The union of two ordinal numbers is an ordinal number. (Contributed by Jim Kingdon, 25-Jul-2019.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∪ 𝐵) ∈ On) | ||
Theorem | onun2i 4462 | The union of two ordinal numbers is an ordinal number. (Contributed by NM, 13-Jun-1994.) (Constructive proof by Jim Kingdon, 25-Jul-2019.) |
⊢ 𝐴 ∈ On & ⊢ 𝐵 ∈ On ⇒ ⊢ (𝐴 ∪ 𝐵) ∈ On | ||
Theorem | ordsson 4463 | 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 𝐴 → 𝐴 ⊆ On) | ||
Theorem | onss 4464 | An ordinal number is a subset of the class of ordinal numbers. (Contributed by NM, 5-Jun-1994.) |
⊢ (𝐴 ∈ On → 𝐴 ⊆ On) | ||
Theorem | onuni 4465 | The union of an ordinal number is an ordinal number. (Contributed by NM, 29-Sep-2006.) |
⊢ (𝐴 ∈ On → ∪ 𝐴 ∈ On) | ||
Theorem | orduni 4466 | The union of an ordinal class is ordinal. (Contributed by NM, 12-Sep-2003.) |
⊢ (Ord 𝐴 → Ord ∪ 𝐴) | ||
Theorem | bm2.5ii 4467* | Problem 2.5(ii) of [BellMachover] p. 471. (Contributed by NM, 20-Sep-2003.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ⊆ On → ∪ 𝐴 = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥}) | ||
Theorem | sucexb 4468 | A successor exists iff its class argument exists. (Contributed by NM, 22-Jun-1998.) |
⊢ (𝐴 ∈ V ↔ suc 𝐴 ∈ V) | ||
Theorem | sucexg 4469 | The successor of a set is a set (generalization). (Contributed by NM, 5-Jun-1994.) |
⊢ (𝐴 ∈ 𝑉 → suc 𝐴 ∈ V) | ||
Theorem | sucex 4470 | The successor of a set is a set. (Contributed by NM, 30-Aug-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ suc 𝐴 ∈ V | ||
Theorem | ordsucim 4471 | The successor of an ordinal class is ordinal. (Contributed by Jim Kingdon, 8-Nov-2018.) |
⊢ (Ord 𝐴 → Ord suc 𝐴) | ||
Theorem | suceloni 4472 | The successor of an ordinal number is an ordinal number. Proposition 7.24 of [TakeutiZaring] p. 41. (Contributed by NM, 6-Jun-1994.) |
⊢ (𝐴 ∈ On → suc 𝐴 ∈ On) | ||
Theorem | ordsucg 4473 | The successor of an ordinal class is ordinal. (Contributed by Jim Kingdon, 20-Nov-2018.) |
⊢ (𝐴 ∈ V → (Ord 𝐴 ↔ Ord suc 𝐴)) | ||
Theorem | sucelon 4474 | The successor of an ordinal number is an ordinal number. (Contributed by NM, 9-Sep-2003.) |
⊢ (𝐴 ∈ On ↔ suc 𝐴 ∈ On) | ||
Theorem | ordsucss 4475 | The successor of an element of an ordinal class is a subset of it. (Contributed by NM, 21-Jun-1998.) |
⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵)) | ||
Theorem | ordelsuc 4476 | 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.) |
⊢ ((𝐴 ∈ 𝐶 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ⊆ 𝐵)) | ||
Theorem | onsucssi 4477 | A set belongs to an ordinal number iff its successor is a subset of the ordinal number. Exercise 8 of [TakeutiZaring] p. 42 and its converse. (Contributed by NM, 16-Sep-1995.) |
⊢ 𝐴 ∈ On & ⊢ 𝐵 ∈ On ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ suc 𝐴 ⊆ 𝐵) | ||
Theorem | onsucmin 4478* | The successor of an ordinal number is the smallest larger ordinal number. (Contributed by NM, 28-Nov-2003.) |
⊢ (𝐴 ∈ On → suc 𝐴 = ∩ {𝑥 ∈ On ∣ 𝐴 ∈ 𝑥}) | ||
Theorem | onsucelsucr 4479 | Membership is inherited by predecessors. The converse, for all ordinals, implies excluded middle, as shown at onsucelsucexmid 4501. However, the converse does hold where 𝐵 is a natural number, as seen at nnsucelsuc 6450. (Contributed by Jim Kingdon, 17-Jul-2019.) |
⊢ (𝐵 ∈ On → (suc 𝐴 ∈ suc 𝐵 → 𝐴 ∈ 𝐵)) | ||
Theorem | onsucsssucr 4480 | The subclass relationship between two ordinals is inherited by their predecessors. The converse implies excluded middle, as shown at onsucsssucexmid 4498. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2019.) |
⊢ ((𝐴 ∈ On ∧ Ord 𝐵) → (suc 𝐴 ⊆ suc 𝐵 → 𝐴 ⊆ 𝐵)) | ||
Theorem | sucunielr 4481 | Successor and union. The converse (where 𝐵 is an ordinal) implies excluded middle, as seen at ordsucunielexmid 4502. (Contributed by Jim Kingdon, 2-Aug-2019.) |
⊢ (suc 𝐴 ∈ 𝐵 → 𝐴 ∈ ∪ 𝐵) | ||
Theorem | unon 4482 | 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 4483* | The union of the ordinal subsets of an ordinal number is that number. (Contributed by Jim Kingdon, 2-Aug-2019.) |
⊢ (𝐴 ∈ On → ∪ {𝑥 ∈ On ∣ 𝑥 ⊆ 𝐴} = 𝐴) | ||
Theorem | limon 4484 | The class of ordinal numbers is a limit ordinal. (Contributed by NM, 24-Mar-1995.) |
⊢ Lim On | ||
Theorem | ordunisuc2r 4485* | An ordinal which contains the successor of each of its members is equal to its union. (Contributed by Jim Kingdon, 14-Nov-2018.) |
⊢ (Ord 𝐴 → (∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 → 𝐴 = ∪ 𝐴)) | ||
Theorem | onssi 4486 | An ordinal number is a subset of On. (Contributed by NM, 11-Aug-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ 𝐴 ⊆ On | ||
Theorem | onsuci 4487 | The successor of an ordinal number is an ordinal number. Corollary 7N(c) of [Enderton] p. 193. (Contributed by NM, 12-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ suc 𝐴 ∈ On | ||
Theorem | onintonm 4488* | The intersection of an inhabited collection of ordinal numbers is an ordinal number. Compare Exercise 6 of [TakeutiZaring] p. 44. (Contributed by Mario Carneiro and Jim Kingdon, 30-Aug-2021.) |
⊢ ((𝐴 ⊆ On ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∩ 𝐴 ∈ On) | ||
Theorem | onintrab2im 4489 | An existence condition which implies an intersection is an ordinal number. (Contributed by Jim Kingdon, 30-Aug-2021.) |
⊢ (∃𝑥 ∈ On 𝜑 → ∩ {𝑥 ∈ On ∣ 𝜑} ∈ On) | ||
Theorem | ordtriexmidlem 4490 | Lemma for decidability and ordinals. The set {𝑥 ∈ {∅} ∣ 𝜑} is a way of connecting statements about ordinals (such as trichotomy in ordtriexmid 4492 or weak linearity in ordsoexmid 4533) with a proposition 𝜑. Our lemma states that it is an ordinal number. (Contributed by Jim Kingdon, 28-Jan-2019.) |
⊢ {𝑥 ∈ {∅} ∣ 𝜑} ∈ On | ||
Theorem | ordtriexmidlem2 4491* | Lemma for decidability and ordinals. The set {𝑥 ∈ {∅} ∣ 𝜑} is a way of connecting statements about ordinals (such as trichotomy in ordtriexmid 4492 or weak linearity in ordsoexmid 4533) with a proposition 𝜑. Our lemma helps connect that set to excluded middle. (Contributed by Jim Kingdon, 28-Jan-2019.) |
⊢ ({𝑥 ∈ {∅} ∣ 𝜑} = ∅ → ¬ 𝜑) | ||
Theorem | ordtriexmid 4492* |
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". Also see exmidontri 7186 which is much the same theorem but biconditionalized and using the EXMID notation. (Contributed by Mario Carneiro and Jim Kingdon, 14-Nov-2018.) |
⊢ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ⇒ ⊢ (𝜑 ∨ ¬ 𝜑) | ||
Theorem | ontriexmidim 4493* | Ordinal trichotomy implies excluded middle. Closed form of ordtriexmid 4492. (Contributed by Jim Kingdon, 26-Aug-2024.) |
⊢ (∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → DECID 𝜑) | ||
Theorem | ordtri2orexmid 4494* | Ordinal trichotomy implies excluded middle. (Contributed by Jim Kingdon, 31-Jul-2019.) |
⊢ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑦 ⊆ 𝑥) ⇒ ⊢ (𝜑 ∨ ¬ 𝜑) | ||
Theorem | 2ordpr 4495 | Version of 2on 6384 with the definition of 2o expanded and expressed in terms of Ord. (Contributed by Jim Kingdon, 29-Aug-2021.) |
⊢ Ord {∅, {∅}} | ||
Theorem | ontr2exmid 4496* | An ordinal transitivity law which implies excluded middle. (Contributed by Jim Kingdon, 17-Sep-2021.) |
⊢ ∀𝑥 ∈ On ∀𝑦∀𝑧 ∈ On ((𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝑧) → 𝑥 ∈ 𝑧) ⇒ ⊢ (𝜑 ∨ ¬ 𝜑) | ||
Theorem | ordtri2or2exmidlem 4497* | A set which is 2o if 𝜑 or ∅ if ¬ 𝜑 is an ordinal. (Contributed by Jim Kingdon, 29-Aug-2021.) |
⊢ {𝑥 ∈ {∅, {∅}} ∣ 𝜑} ∈ On | ||
Theorem | onsucsssucexmid 4498* | The converse of onsucsssucr 4480 implies excluded middle. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2019.) |
⊢ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ⊆ 𝑦 → suc 𝑥 ⊆ suc 𝑦) ⇒ ⊢ (𝜑 ∨ ¬ 𝜑) | ||
Theorem | onsucelsucexmidlem1 4499* | Lemma for onsucelsucexmid 4501. (Contributed by Jim Kingdon, 2-Aug-2019.) |
⊢ ∅ ∈ {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)} | ||
Theorem | onsucelsucexmidlem 4500* | Lemma for onsucelsucexmid 4501. The set {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)} appears as 𝐴 in the proof of Theorem 1.3 in [Bauer] p. 483 (see acexmidlema 5827), and similar sets also appear in other proofs that various propositions imply excluded middle, for example in ordtriexmidlem 4490. (Contributed by Jim Kingdon, 2-Aug-2019.) |
⊢ {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)} ∈ On |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |