Home Intuitionistic Logic ExplorerTheorem List (p. 44 of 136) < 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 - 4301-4400   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremfreq2 4301 Equality theorem for the well-founded predicate. (Contributed by NM, 3-Apr-1994.)
(𝐴 = 𝐵 → (𝑅 Fr 𝐴𝑅 Fr 𝐵))

Theoremfrforeq3 4302 Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.)
(𝑆 = 𝑇 → ( FrFor 𝑅𝐴𝑆 ↔ FrFor 𝑅𝐴𝑇))

Theoremnffrfor 4303 Bound-variable hypothesis builder for well-founded relations. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario Carneiro, 14-Oct-2016.)
𝑥𝑅    &   𝑥𝐴    &   𝑥𝑆       𝑥 FrFor 𝑅𝐴𝑆

Theoremnffr 4304 Bound-variable hypothesis builder for well-founded relations. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario Carneiro, 14-Oct-2016.)
𝑥𝑅    &   𝑥𝐴       𝑥 𝑅 Fr 𝐴

Theoremfrirrg 4305 A well-founded relation is irreflexive. This is the case where 𝐴 exists. (Contributed by Jim Kingdon, 21-Sep-2021.)
((𝑅 Fr 𝐴𝐴𝑉𝐵𝐴) → ¬ 𝐵𝑅𝐵)

Theoremfr0 4306 Any relation is well-founded on the empty set. (Contributed by NM, 17-Sep-1993.)
𝑅 Fr ∅

Theoremfrind 4307* Induction over a well-founded set. (Contributed by Jim Kingdon, 28-Sep-2021.)
(𝑥 = 𝑦 → (𝜑𝜓))    &   ((𝜒𝑥𝐴) → (∀𝑦𝐴 (𝑦𝑅𝑥𝜓) → 𝜑))    &   (𝜒𝑅 Fr 𝐴)    &   (𝜒𝐴𝑉)       ((𝜒𝑥𝐴) → 𝜑)

Theoremefrirr 4308 Irreflexivity of the epsilon relation: a class founded by epsilon is not a member of itself. (Contributed by NM, 18-Apr-1994.) (Revised by Mario Carneiro, 22-Jun-2015.)
( E Fr 𝐴 → ¬ 𝐴𝐴)

Theoremtz7.2 4309 Similar to Theorem 7.2 of [TakeutiZaring] p. 35, of except that the Axiom of Regularity is not required due to antecedent E Fr 𝐴. (Contributed by NM, 4-May-1994.)
((Tr 𝐴 ∧ E Fr 𝐴𝐵𝐴) → (𝐵𝐴𝐵𝐴))

Theoremnfwe 4310 Bound-variable hypothesis builder for well-orderings. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario Carneiro, 14-Oct-2016.)
𝑥𝑅    &   𝑥𝐴       𝑥 𝑅 We 𝐴

Theoremweeq1 4311 Equality theorem for the well-ordering predicate. (Contributed by NM, 9-Mar-1997.)
(𝑅 = 𝑆 → (𝑅 We 𝐴𝑆 We 𝐴))

Theoremweeq2 4312 Equality theorem for the well-ordering predicate. (Contributed by NM, 3-Apr-1994.)
(𝐴 = 𝐵 → (𝑅 We 𝐴𝑅 We 𝐵))

Theoremwefr 4313 A well-ordering is well-founded. (Contributed by NM, 22-Apr-1994.)
(𝑅 We 𝐴𝑅 Fr 𝐴)

Theoremwepo 4314 A well-ordering is a partial ordering. (Contributed by Jim Kingdon, 23-Sep-2021.)
((𝑅 We 𝐴𝐴𝑉) → 𝑅 Po 𝐴)

Theoremwetrep 4315* An epsilon well-ordering is a transitive relation. (Contributed by NM, 22-Apr-1994.)
(( E We 𝐴 ∧ (𝑥𝐴𝑦𝐴𝑧𝐴)) → ((𝑥𝑦𝑦𝑧) → 𝑥𝑧))

Theoremwe0 4316 Any relation is a well-ordering of the empty set. (Contributed by NM, 16-Mar-1997.)
𝑅 We ∅

2.3.10  Ordinals

Syntaxword 4317 Extend the definition of a wff to include the ordinal predicate.
wff Ord 𝐴

Syntaxcon0 4318 Extend the definition of a class to include the class of all ordinal numbers. (The 0 in the name prevents creating a file called con.html, which causes problems in Windows.)
class On

Syntaxwlim 4319 Extend the definition of a wff to include the limit ordinal predicate.
wff Lim 𝐴

Syntaxcsuc 4320 Extend class notation to include the successor function.
class suc 𝐴

Definitiondf-iord 4321* Define the ordinal predicate, which is true for a class that is transitive and whose elements are transitive. Definition of ordinal in [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic". (Contributed by Jim Kingdon, 10-Oct-2018.) Use its alias dford3 4322 instead for naming consistency with set.mm. (New usage is discouraged.)
(Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥𝐴 Tr 𝑥))

Theoremdford3 4322* Alias for df-iord 4321. Use it instead of df-iord 4321 for naming consistency with set.mm. (Contributed by Jim Kingdon, 10-Oct-2018.)
(Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥𝐴 Tr 𝑥))

Definitiondf-on 4323 Define the class of all ordinal numbers. Definition 7.11 of [TakeutiZaring] p. 38. (Contributed by NM, 5-Jun-1994.)
On = {𝑥 ∣ Ord 𝑥}

Definitiondf-ilim 4324 Define the limit ordinal predicate, which is true for an ordinal that has the empty set as an element and is not a successor (i.e. that is the union of itself). Our definition combines the definition of Lim of [BellMachover] p. 471 and Exercise 1 of [TakeutiZaring] p. 42, and then changes 𝐴 ≠ ∅ to ∅ ∈ 𝐴 (which would be equivalent given the law of the excluded middle, but which is not for us). (Contributed by Jim Kingdon, 11-Nov-2018.) Use its alias dflim2 4325 instead for naming consistency with set.mm. (New usage is discouraged.)
(Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴𝐴 = 𝐴))

Theoremdflim2 4325 Alias for df-ilim 4324. Use it instead of df-ilim 4324 for naming consistency with set.mm. (Contributed by NM, 4-Nov-2004.)
(Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴𝐴 = 𝐴))

Definitiondf-suc 4326 Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1". Definition 7.22 of [TakeutiZaring] p. 41, who use "+ 1" to denote this function. Our definition is a generalization to classes. Although it is not conventional to use it with proper classes, it has no effect on a proper class (sucprc 4367). Some authors denote the successor operation with a prime (apostrophe-like) symbol, such as Definition 6 of [Suppes] p. 134 and the definition of successor in [Mendelson] p. 246 (who uses the symbol "Suc" as a predicate to mean "is a successor ordinal"). The definition of successor of [Enderton] p. 68 denotes the operation with a plus-sign superscript. (Contributed by NM, 30-Aug-1993.)
suc 𝐴 = (𝐴 ∪ {𝐴})

Theoremordeq 4327 Equality theorem for the ordinal predicate. (Contributed by NM, 17-Sep-1993.)
(𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))

Theoremelong 4328 An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.)
(𝐴𝑉 → (𝐴 ∈ On ↔ Ord 𝐴))

Theoremelon 4329 An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.)
𝐴 ∈ V       (𝐴 ∈ On ↔ Ord 𝐴)

Theoremeloni 4330 An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994.)
(𝐴 ∈ On → Ord 𝐴)

Theoremelon2 4331 An ordinal number is an ordinal set. (Contributed by NM, 8-Feb-2004.)
(𝐴 ∈ On ↔ (Ord 𝐴𝐴 ∈ V))

Theoremlimeq 4332 Equality theorem for the limit predicate. (Contributed by NM, 22-Apr-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵))

Theoremordtr 4333 An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.)
(Ord 𝐴 → Tr 𝐴)

Theoremordelss 4334 An element of an ordinal class is a subset of it. (Contributed by NM, 30-May-1994.)
((Ord 𝐴𝐵𝐴) → 𝐵𝐴)

Theoremtrssord 4335 A transitive subclass of an ordinal class is ordinal. (Contributed by NM, 29-May-1994.)
((Tr 𝐴𝐴𝐵 ∧ Ord 𝐵) → Ord 𝐴)

Theoremordelord 4336 An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. (Contributed by NM, 23-Apr-1994.)
((Ord 𝐴𝐵𝐴) → Ord 𝐵)

Theoremtron 4337 The class of all ordinal numbers is transitive. (Contributed by NM, 4-May-2009.)
Tr On

Theoremordelon 4338 An element of an ordinal class is an ordinal number. (Contributed by NM, 26-Oct-2003.)
((Ord 𝐴𝐵𝐴) → 𝐵 ∈ On)

Theoremonelon 4339 An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of [BellMachover] p. 469. (Contributed by NM, 26-Oct-2003.)
((𝐴 ∈ On ∧ 𝐵𝐴) → 𝐵 ∈ On)

Theoremordin 4340 The intersection of two ordinal classes is ordinal. Proposition 7.9 of [TakeutiZaring] p. 37. (Contributed by NM, 9-May-1994.)
((Ord 𝐴 ∧ Ord 𝐵) → Ord (𝐴𝐵))

Theoremonin 4341 The intersection of two ordinal numbers is an ordinal number. (Contributed by NM, 7-Apr-1995.)
((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴𝐵) ∈ On)

Theoremonelss 4342 An element of an ordinal number is a subset of the number. (Contributed by NM, 5-Jun-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(𝐴 ∈ On → (𝐵𝐴𝐵𝐴))

Theoremordtr1 4343 Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.)
(Ord 𝐶 → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))

Theoremontr1 4344 Transitive law for ordinal numbers. Theorem 7M(b) of [Enderton] p. 192. (Contributed by NM, 11-Aug-1994.)
(𝐶 ∈ On → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))

Theoremonintss 4345* If a property is true for an ordinal number, then the minimum ordinal number for which it is true is smaller or equal. Theorem Schema 61 of [Suppes] p. 228. (Contributed by NM, 3-Oct-2003.)
(𝑥 = 𝐴 → (𝜑𝜓))       (𝐴 ∈ On → (𝜓 {𝑥 ∈ On ∣ 𝜑} ⊆ 𝐴))

Theoremord0 4346 The empty set is an ordinal class. (Contributed by NM, 11-May-1994.)
Ord ∅

Theorem0elon 4347 The empty set is an ordinal number. Corollary 7N(b) of [Enderton] p. 193. (Contributed by NM, 17-Sep-1993.)
∅ ∈ On

Theoreminton 4348 The intersection of the class of ordinal numbers is the empty set. (Contributed by NM, 20-Oct-2003.)
On = ∅

Theoremnlim0 4349 The empty set is not a limit ordinal. (Contributed by NM, 24-Mar-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
¬ Lim ∅

Theoremlimord 4350 A limit ordinal is ordinal. (Contributed by NM, 4-May-1995.)
(Lim 𝐴 → Ord 𝐴)

Theoremlimuni 4351 A limit ordinal is its own supremum (union). (Contributed by NM, 4-May-1995.)
(Lim 𝐴𝐴 = 𝐴)

Theoremlimuni2 4352 The union of a limit ordinal is a limit ordinal. (Contributed by NM, 19-Sep-2006.)
(Lim 𝐴 → Lim 𝐴)

Theorem0ellim 4353 A limit ordinal contains the empty set. (Contributed by NM, 15-May-1994.)
(Lim 𝐴 → ∅ ∈ 𝐴)

Theoremlimelon 4354 A limit ordinal class that is also a set is an ordinal number. (Contributed by NM, 26-Apr-2004.)
((𝐴𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On)

Theoremonn0 4355 The class of all ordinal numbers is not empty. (Contributed by NM, 17-Sep-1995.)
On ≠ ∅

Theoremonm 4356 The class of all ordinal numbers is inhabited. (Contributed by Jim Kingdon, 6-Mar-2019.)
𝑥 𝑥 ∈ On

Theoremsuceq 4357 Equality of successors. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Theoremelsuci 4358 Membership in a successor. This one-way implication does not require that either 𝐴 or 𝐵 be sets. (Contributed by NM, 6-Jun-1994.)
(𝐴 ∈ suc 𝐵 → (𝐴𝐵𝐴 = 𝐵))

Theoremelsucg 4359 Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 15-Sep-1995.)
(𝐴𝑉 → (𝐴 ∈ suc 𝐵 ↔ (𝐴𝐵𝐴 = 𝐵)))

Theoremelsuc2g 4360 Variant of membership in a successor, requiring that 𝐵 rather than 𝐴 be a set. (Contributed by NM, 28-Oct-2003.)
(𝐵𝑉 → (𝐴 ∈ suc 𝐵 ↔ (𝐴𝐵𝐴 = 𝐵)))

Theoremelsuc 4361 Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 15-Sep-2003.)
𝐴 ∈ V       (𝐴 ∈ suc 𝐵 ↔ (𝐴𝐵𝐴 = 𝐵))

Theoremelsuc2 4362 Membership in a successor. (Contributed by NM, 15-Sep-2003.)
𝐴 ∈ V       (𝐵 ∈ suc 𝐴 ↔ (𝐵𝐴𝐵 = 𝐴))

Theoremnfsuc 4363 Bound-variable hypothesis builder for successor. (Contributed by NM, 15-Sep-2003.)
𝑥𝐴       𝑥 suc 𝐴

Theoremelelsuc 4364 Membership in a successor. (Contributed by NM, 20-Jun-1998.)
(𝐴𝐵𝐴 ∈ suc 𝐵)

Theoremsucel 4365* Membership of a successor in another class. (Contributed by NM, 29-Jun-2004.)
(suc 𝐴𝐵 ↔ ∃𝑥𝐵𝑦(𝑦𝑥 ↔ (𝑦𝐴𝑦 = 𝐴)))

Theoremsuc0 4366 The successor of the empty set. (Contributed by NM, 1-Feb-2005.)
suc ∅ = {∅}

Theoremsucprc 4367 A proper class is its own successor. (Contributed by NM, 3-Apr-1995.)
𝐴 ∈ V → suc 𝐴 = 𝐴)

Theoremunisuc 4368 A transitive class is equal to the union of its successor. Combines Theorem 4E of [Enderton] p. 72 and Exercise 6 of [Enderton] p. 73. (Contributed by NM, 30-Aug-1993.)
𝐴 ∈ V       (Tr 𝐴 suc 𝐴 = 𝐴)

Theoremunisucg 4369 A transitive class is equal to the union of its successor. Combines Theorem 4E of [Enderton] p. 72 and Exercise 6 of [Enderton] p. 73. (Contributed by Jim Kingdon, 18-Aug-2019.)
(𝐴𝑉 → (Tr 𝐴 suc 𝐴 = 𝐴))

Theoremsssucid 4370 A class is included in its own successor. Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized to arbitrary classes). (Contributed by NM, 31-May-1994.)
𝐴 ⊆ suc 𝐴

Theoremsucidg 4371 Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized). (Contributed by NM, 25-Mar-1995.) (Proof shortened by Scott Fenton, 20-Feb-2012.)
(𝐴𝑉𝐴 ∈ suc 𝐴)

Theoremsucid 4372 A set belongs to its successor. (Contributed by NM, 22-Jun-1994.) (Proof shortened by Alan Sare, 18-Feb-2012.) (Proof shortened by Scott Fenton, 20-Feb-2012.)
𝐴 ∈ V       𝐴 ∈ suc 𝐴

Theoremnsuceq0g 4373 No successor is empty. (Contributed by Jim Kingdon, 14-Oct-2018.)
(𝐴𝑉 → suc 𝐴 ≠ ∅)

Theoremeqelsuc 4374 A set belongs to the successor of an equal set. (Contributed by NM, 18-Aug-1994.)
𝐴 ∈ V       (𝐴 = 𝐵𝐴 ∈ suc 𝐵)

Theoremiunsuc 4375* Inductive definition for the indexed union at a successor. (Contributed by Mario Carneiro, 4-Feb-2013.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
𝐴 ∈ V    &   (𝑥 = 𝐴𝐵 = 𝐶)        𝑥 ∈ suc 𝐴𝐵 = ( 𝑥𝐴 𝐵𝐶)

Theoremsuctr 4376 The successor of a transitive class is transitive. (Contributed by Alan Sare, 11-Apr-2009.)
(Tr 𝐴 → Tr suc 𝐴)

Theoremtrsuc 4377 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 𝐴 ∧ suc 𝐵𝐴) → 𝐵𝐴)

Theoremtrsucss 4378 A member of the successor of a transitive class is a subclass of it. (Contributed by NM, 4-Oct-2003.)
(Tr 𝐴 → (𝐵 ∈ suc 𝐴𝐵𝐴))

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

Theoremorduniss 4380 An ordinal class includes its union. (Contributed by NM, 13-Sep-2003.)
(Ord 𝐴 𝐴𝐴)

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

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

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

Theoremonelssi 4384 A member of an ordinal number is a subset of it. (Contributed by NM, 11-Aug-1994.)
𝐴 ∈ On       (𝐵𝐴𝐵𝐴)

Theoremonelini 4385 An element of an ordinal number equals the intersection with it. (Contributed by NM, 11-Jun-1994.)
𝐴 ∈ On       (𝐵𝐴𝐵 = (𝐵𝐴))

Theoremoneluni 4386 An ordinal number equals its union with any element. (Contributed by NM, 13-Jun-1994.)
𝐴 ∈ On       (𝐵𝐴 → (𝐴𝐵) = 𝐴)

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

2.4  IZF Set Theory - add the Axiom of Union

2.4.1  Introduce the Axiom of Union

Axiomax-un 4388* 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 4390 states that the union itself exists. A version with the standard abbreviation for union is uniex2 4391. A version using class notation is uniex 4392.

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 4081), and (c) the order of the conjuncts is swapped (which is equivalent by ancom 264).

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

𝑦𝑧(∃𝑤(𝑧𝑤𝑤𝑥) → 𝑧𝑦)

Theoremzfun 4389* Axiom of Union expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.)
𝑥𝑦(∃𝑥(𝑦𝑥𝑥𝑧) → 𝑦𝑥)

Theoremaxun2 4390* A variant of the Axiom of Union ax-un 4388. 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.)
𝑦𝑧(𝑧𝑦 ↔ ∃𝑤(𝑧𝑤𝑤𝑥))

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

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

Theoremvuniex 4393 The union of a setvar is a set. (Contributed by BJ, 3-May-2021.)
𝑥 ∈ V

Theoremuniexg 4394 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)

Theoremunex 4395 The union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 1-Jul-1994.)
𝐴 ∈ V    &   𝐵 ∈ V       (𝐴𝐵) ∈ V

Theoremunexb 4396 Existence of union is equivalent to existence of its components. (Contributed by NM, 11-Jun-1998.)
((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴𝐵) ∈ V)

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

Theoremtpexg 4398 An unordered triple of classes exists. (Contributed by NM, 10-Apr-1994.)
((𝐴𝑈𝐵𝑉𝐶𝑊) → {𝐴, 𝐵, 𝐶} ∈ V)

Theoremunisn3 4399* Union of a singleton in the form of a restricted class abstraction. (Contributed by NM, 3-Jul-2008.)
(𝐴𝐵 {𝑥𝐵𝑥 = 𝐴} = 𝐴)

Theoremabnexg 4400* 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 6056. Note that the second antecedent 𝑥𝐴𝑥𝐹 cannot be translated to 𝐴𝐹 since 𝐹 may depend on 𝑥. In applications, one may take 𝐹 = {𝑥} or 𝐹 = 𝒫 𝑥 (see snnex 4402 and pwnex 4403 respectively, proved from abnex 4401, which is a consequence of abnexg 4400 with 𝐴 = V). (Contributed by BJ, 2-Dec-2021.)
(∀𝑥𝐴 (𝐹𝑉𝑥𝐹) → ({𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐹} ∈ 𝑊𝐴 ∈ V))

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-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13593
 Copyright terms: Public domain < Previous  Next >