Home | Metamath
Proof Explorer Theorem List (p. 95 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | oiiso2 9401 | The order isomorphism of the well-order π on π΄ is an isomorphism onto ran π (which is a subset of π΄ by oif 9400). (Contributed by Mario Carneiro, 25-Jun-2015.) |
β’ πΉ = OrdIso(π , π΄) β β’ ((π We π΄ β§ π Se π΄) β πΉ Isom E , π (dom πΉ, ran πΉ)) | ||
Theorem | ordtype 9402 | For any set-like well-ordered class, there is an isomorphic ordinal number called its order type. (Contributed by Jeff Hankins, 17-Oct-2009.) (Revised by Mario Carneiro, 25-Jun-2015.) |
β’ πΉ = OrdIso(π , π΄) β β’ ((π We π΄ β§ π Se π΄) β πΉ Isom E , π (dom πΉ, π΄)) | ||
Theorem | oiiniseg 9403 | ran πΉ is an initial segment of π΄ under the well-order π . (Contributed by Mario Carneiro, 26-Jun-2015.) |
β’ πΉ = OrdIso(π , π΄) β β’ (((π We π΄ β§ π Se π΄) β§ (π β π΄ β§ π β dom πΉ)) β ((πΉβπ)π π β¨ π β ran πΉ)) | ||
Theorem | ordtype2 9404 | For any set-like well-ordered class, if the order isomorphism exists (is a set), then it maps some ordinal onto π΄ isomorphically. Otherwise, πΉ is a proper class, which implies that either ran πΉ β π΄ is a proper class or dom πΉ = On. This weak version of ordtype 9402 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 25-Jun-2015.) |
β’ πΉ = OrdIso(π , π΄) β β’ ((π We π΄ β§ π Se π΄ β§ πΉ β V) β πΉ Isom E , π (dom πΉ, π΄)) | ||
Theorem | oiexg 9405 | The order isomorphism on a set is a set. (Contributed by Mario Carneiro, 25-Jun-2015.) |
β’ πΉ = OrdIso(π , π΄) β β’ (π΄ β π β πΉ β V) | ||
Theorem | oion 9406 | The order type of the well-order π on π΄ is an ordinal. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 23-May-2015.) |
β’ πΉ = OrdIso(π , π΄) β β’ (π΄ β π β dom πΉ β On) | ||
Theorem | oiiso 9407 | The order isomorphism of the well-order π on π΄ is an isomorphism. (Contributed by Mario Carneiro, 23-May-2015.) |
β’ πΉ = OrdIso(π , π΄) β β’ ((π΄ β π β§ π We π΄) β πΉ Isom E , π (dom πΉ, π΄)) | ||
Theorem | oien 9408 | The order type of a well-ordered set is equinumerous to the set. (Contributed by Mario Carneiro, 23-May-2015.) |
β’ πΉ = OrdIso(π , π΄) β β’ ((π΄ β π β§ π We π΄) β dom πΉ β π΄) | ||
Theorem | oieu 9409 | Uniqueness of the unique ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015.) (Revised by Mario Carneiro, 25-Jun-2015.) |
β’ πΉ = OrdIso(π , π΄) β β’ ((π We π΄ β§ π Se π΄) β ((Ord π΅ β§ πΊ Isom E , π (π΅, π΄)) β (π΅ = dom πΉ β§ πΊ = πΉ))) | ||
Theorem | oismo 9410 | When π΄ is a subclass of On, πΉ is a strictly monotone ordinal functions, and it is also complete (it is an isomorphism onto all of π΄). The proof avoids ax-rep 5241 (the second statement is trivial under ax-rep 5241). (Contributed by Mario Carneiro, 26-Jun-2015.) |
β’ πΉ = OrdIso( E , π΄) β β’ (π΄ β On β (Smo πΉ β§ ran πΉ = π΄)) | ||
Theorem | oiid 9411 | The order type of an ordinal under the β order is itself, and the order isomorphism is the identity function. (Contributed by Mario Carneiro, 26-Jun-2015.) |
β’ (Ord π΄ β OrdIso( E , π΄) = ( I βΎ π΄)) | ||
Theorem | hartogslem1 9412* | Lemma for hartogs 9414. (Contributed by Mario Carneiro, 14-Jan-2013.) (Revised by Mario Carneiro, 15-May-2015.) |
β’ πΉ = {β¨π, π¦β© β£ (((dom π β π΄ β§ ( I βΎ dom π) β π β§ π β (dom π Γ dom π)) β§ (π β I ) We dom π) β§ π¦ = dom OrdIso((π β I ), dom π))} & β’ π = {β¨π , π‘β© β£ βπ€ β π¦ βπ§ β π¦ ((π = (πβπ€) β§ π‘ = (πβπ§)) β§ π€ E π§)} β β’ (dom πΉ β π« (π΄ Γ π΄) β§ Fun πΉ β§ (π΄ β π β ran πΉ = {π₯ β On β£ π₯ βΌ π΄})) | ||
Theorem | hartogslem2 9413* | Lemma for hartogs 9414. (Contributed by Mario Carneiro, 14-Jan-2013.) |
β’ πΉ = {β¨π, π¦β© β£ (((dom π β π΄ β§ ( I βΎ dom π) β π β§ π β (dom π Γ dom π)) β§ (π β I ) We dom π) β§ π¦ = dom OrdIso((π β I ), dom π))} & β’ π = {β¨π , π‘β© β£ βπ€ β π¦ βπ§ β π¦ ((π = (πβπ€) β§ π‘ = (πβπ§)) β§ π€ E π§)} β β’ (π΄ β π β {π₯ β On β£ π₯ βΌ π΄} β V) | ||
Theorem | hartogs 9414* | The class of ordinals dominated by a given set is an ordinal. A shorter (when taking into account lemmas hartogslem1 9412 and hartogslem2 9413) proof can be given using the axiom of choice, see ondomon 10433. As its label indicates, this result is used to justify the definition of the Hartogs function df-har 9427. (Contributed by Jeff Hankins, 22-Oct-2009.) (Revised by Mario Carneiro, 15-May-2015.) |
β’ (π΄ β π β {π₯ β On β£ π₯ βΌ π΄} β On) | ||
Theorem | wofib 9415 | The only sets which are well-ordered forwards and backwards are finite sets. (Contributed by Mario Carneiro, 30-Jan-2014.) (Revised by Mario Carneiro, 23-May-2015.) |
β’ π΄ β V β β’ ((π Or π΄ β§ π΄ β Fin) β (π We π΄ β§ β‘π We π΄)) | ||
Theorem | wemaplem1 9416* | Value of the lexicographic order on a sequence space. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
β’ π = {β¨π₯, π¦β© β£ βπ§ β π΄ ((π₯βπ§)π(π¦βπ§) β§ βπ€ β π΄ (π€π π§ β (π₯βπ€) = (π¦βπ€)))} β β’ ((π β π β§ π β π) β (πππ β βπ β π΄ ((πβπ)π(πβπ) β§ βπ β π΄ (ππ π β (πβπ) = (πβπ))))) | ||
Theorem | wemaplem2 9417* | Lemma for wemapso 9421. Transitivity. (Contributed by Stefan O'Rear, 17-Jan-2015.) (Revised by AV, 21-Jul-2024.) |
β’ π = {β¨π₯, π¦β© β£ βπ§ β π΄ ((π₯βπ§)π(π¦βπ§) β§ βπ€ β π΄ (π€π π§ β (π₯βπ€) = (π¦βπ€)))} & β’ (π β π β (π΅ βm π΄)) & β’ (π β π β (π΅ βm π΄)) & β’ (π β π β (π΅ βm π΄)) & β’ (π β π Or π΄) & β’ (π β π Po π΅) & β’ (π β π β π΄) & β’ (π β (πβπ)π(πβπ)) & β’ (π β βπ β π΄ (ππ π β (πβπ) = (πβπ))) & β’ (π β π β π΄) & β’ (π β (πβπ)π(πβπ)) & β’ (π β βπ β π΄ (ππ π β (πβπ) = (πβπ))) β β’ (π β πππ) | ||
Theorem | wemaplem3 9418* | Lemma for wemapso 9421. Transitivity. (Contributed by Stefan O'Rear, 17-Jan-2015.) (Revised by AV, 21-Jul-2024.) |
β’ π = {β¨π₯, π¦β© β£ βπ§ β π΄ ((π₯βπ§)π(π¦βπ§) β§ βπ€ β π΄ (π€π π§ β (π₯βπ€) = (π¦βπ€)))} & β’ (π β π β (π΅ βm π΄)) & β’ (π β π β (π΅ βm π΄)) & β’ (π β π β (π΅ βm π΄)) & β’ (π β π Or π΄) & β’ (π β π Po π΅) & β’ (π β πππ) & β’ (π β πππ) β β’ (π β πππ) | ||
Theorem | wemappo 9419* |
Construct lexicographic order on a function space based on a
well-ordering of the indices and a total ordering of the values.
Without totality on the values or least differing indices, the best we can prove here is a partial order. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by AV, 21-Jul-2024.) |
β’ π = {β¨π₯, π¦β© β£ βπ§ β π΄ ((π₯βπ§)π(π¦βπ§) β§ βπ€ β π΄ (π€π π§ β (π₯βπ€) = (π¦βπ€)))} β β’ ((π Or π΄ β§ π Po π΅) β π Po (π΅ βm π΄)) | ||
Theorem | wemapsolem 9420* | Lemma for wemapso 9421. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 21-Jul-2024.) |
β’ π = {β¨π₯, π¦β© β£ βπ§ β π΄ ((π₯βπ§)π(π¦βπ§) β§ βπ€ β π΄ (π€π π§ β (π₯βπ€) = (π¦βπ€)))} & β’ π β (π΅ βm π΄) & β’ (π β π Or π΄) & β’ (π β π Or π΅) & β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β βπ β dom (π β π)βπ β dom (π β π) Β¬ ππ π) β β’ (π β π Or π) | ||
Theorem | wemapso 9421* | Construct lexicographic order on a function space based on a well-ordering of the indices and a total ordering of the values. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 21-Jul-2024.) |
β’ π = {β¨π₯, π¦β© β£ βπ§ β π΄ ((π₯βπ§)π(π¦βπ§) β§ βπ€ β π΄ (π€π π§ β (π₯βπ€) = (π¦βπ€)))} β β’ ((π We π΄ β§ π Or π΅) β π Or (π΅ βm π΄)) | ||
Theorem | wemapso2lem 9422* | Lemma for wemapso2 9423. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 1-Jul-2019.) |
β’ π = {β¨π₯, π¦β© β£ βπ§ β π΄ ((π₯βπ§)π(π¦βπ§) β§ βπ€ β π΄ (π€π π§ β (π₯βπ€) = (π¦βπ€)))} & β’ π = {π₯ β (π΅ βm π΄) β£ π₯ finSupp π} β β’ (((π΄ β π β§ π Or π΄ β§ π Or π΅) β§ π β π) β π Or π) | ||
Theorem | wemapso2 9423* | An alternative to having a well-order on π in wemapso 9421 is to restrict the function set to finitely-supported functions. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 1-Jul-2019.) |
β’ π = {β¨π₯, π¦β© β£ βπ§ β π΄ ((π₯βπ§)π(π¦βπ§) β§ βπ€ β π΄ (π€π π§ β (π₯βπ€) = (π¦βπ€)))} & β’ π = {π₯ β (π΅ βm π΄) β£ π₯ finSupp π} β β’ ((π΄ β π β§ π Or π΄ β§ π Or π΅) β π Or π) | ||
Theorem | card2on 9424* | The alternate definition of the cardinal of a set given in cardval2 9861 always gives a set, and indeed an ordinal. (Contributed by Mario Carneiro, 14-Jan-2013.) |
β’ {π₯ β On β£ π₯ βΊ π΄} β On | ||
Theorem | card2inf 9425* | The alternate definition of the cardinal of a set given in cardval2 9861 has the curious property that for non-numerable sets (for which ndmfv 6873 yields β ), it still evaluates to a nonempty set, and indeed it contains Ο. (Contributed by Mario Carneiro, 15-Jan-2013.) (Revised by Mario Carneiro, 27-Apr-2015.) |
β’ π΄ β V β β’ (Β¬ βπ¦ β On π¦ β π΄ β Ο β {π₯ β On β£ π₯ βΊ π΄}) | ||
Syntax | char 9426 | Class symbol for the Hartogs function. |
class har | ||
Definition | df-har 9427* |
Define the Hartogs function as mapping a set to the class of ordinals it
dominates. That class is an ordinal by hartogs 9414, which is used in
harf 9428.
The Hartogs number of a set is the least ordinal not dominated by that set. Theorem harval2 9867 proves that the Hartogs function actually gives the Hartogs number for well-orderable sets. The Hartogs number of an ordinal is its cardinal successor. This is proved for finite ordinal in harsucnn 9868. Traditionally, the Hartogs number of a set π is written β΅(π), and its cardinal successor, π +; we use functional notation for this, and cannot use the aleph symbol because it is taken for the enumerating function of the infinite initial ordinals df-aleph 9810. Some authors define the Hartogs number of a set to be the least *infinite* ordinal which does not inject into it, thus causing the range to consist only of alephs. We use the simpler definition where the value can be any successor cardinal. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
β’ har = (π₯ β V β¦ {π¦ β On β£ π¦ βΌ π₯}) | ||
Theorem | harf 9428 | Functionality of the Hartogs function. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
β’ har:VβΆOn | ||
Theorem | harcl 9429 | Values of the Hartogs function are ordinals (closure of the Hartogs function in the ordinals). (Contributed by Stefan O'Rear, 11-Feb-2015.) |
β’ (harβπ) β On | ||
Theorem | harval 9430* | Function value of the Hartogs function. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
β’ (π β π β (harβπ) = {π¦ β On β£ π¦ βΌ π}) | ||
Theorem | elharval 9431 | The Hartogs number of a set contains exactly the ordinals that set dominates. Combined with harcl 9429, this implies that the Hartogs number of a set is greater than all ordinals that set dominates. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 15-May-2015.) |
β’ (π β (harβπ) β (π β On β§ π βΌ π)) | ||
Theorem | harndom 9432 | The Hartogs number of a set does not inject into that set. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 15-May-2015.) |
β’ Β¬ (harβπ) βΌ π | ||
Theorem | harword 9433 | Weak ordering property of the Hartogs function. (Contributed by Stefan O'Rear, 14-Feb-2015.) |
β’ (π βΌ π β (harβπ) β (harβπ)) | ||
Syntax | cwdom 9434 | Class symbol for the weak dominance relation. |
class βΌ* | ||
Definition | df-wdom 9435* | A set is weakly dominated by a "larger" set if the "larger" set can be mapped onto the "smaller" set or the smaller set is empty, or equivalently, if the smaller set can be placed into bijection with some partition of the larger set. Dominance (df-dom 8819) implies weak dominance (over ZF). The principle asserting the converse is known as the partition principle and is independent of ZF. Theorem fodom 10393 proves that the axiom of choice implies the partition principle (over ZF). It is not known whether the partition principle is equivalent to the axiom of choice (over ZF), although it is know to imply dependent choice. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
β’ βΌ* = {β¨π₯, π¦β© β£ (π₯ = β β¨ βπ§ π§:π¦βontoβπ₯)} | ||
Theorem | relwdom 9436 | Weak dominance is a relation. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
β’ Rel βΌ* | ||
Theorem | brwdom 9437* | Property of weak dominance (definitional form). (Contributed by Stefan O'Rear, 11-Feb-2015.) |
β’ (π β π β (π βΌ* π β (π = β β¨ βπ§ π§:πβontoβπ))) | ||
Theorem | brwdomi 9438* | Property of weak dominance, forward direction only. (Contributed by Mario Carneiro, 5-May-2015.) |
β’ (π βΌ* π β (π = β β¨ βπ§ π§:πβontoβπ)) | ||
Theorem | brwdomn0 9439* | Weak dominance over nonempty sets. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
β’ (π β β β (π βΌ* π β βπ§ π§:πβontoβπ)) | ||
Theorem | 0wdom 9440 | Any set weakly dominates the empty set. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
β’ (π β π β β βΌ* π) | ||
Theorem | fowdom 9441 | An onto function implies weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
β’ ((πΉ β π β§ πΉ:πβontoβπ) β π βΌ* π) | ||
Theorem | wdomref 9442 | Reflexivity of weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
β’ (π β π β π βΌ* π) | ||
Theorem | brwdom2 9443* | Alternate characterization of the weak dominance predicate which does not require special treatment of the empty set. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
β’ (π β π β (π βΌ* π β βπ¦ β π« πβπ§ π§:π¦βontoβπ)) | ||
Theorem | domwdom 9444 | Weak dominance is implied by dominance in the usual sense. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
β’ (π βΌ π β π βΌ* π) | ||
Theorem | wdomtr 9445 | Transitivity of weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
β’ ((π βΌ* π β§ π βΌ* π) β π βΌ* π) | ||
Theorem | wdomen1 9446 | Equality-like theorem for equinumerosity and weak dominance. (Contributed by Mario Carneiro, 18-May-2015.) |
β’ (π΄ β π΅ β (π΄ βΌ* πΆ β π΅ βΌ* πΆ)) | ||
Theorem | wdomen2 9447 | Equality-like theorem for equinumerosity and weak dominance. (Contributed by Mario Carneiro, 18-May-2015.) |
β’ (π΄ β π΅ β (πΆ βΌ* π΄ β πΆ βΌ* π΅)) | ||
Theorem | wdompwdom 9448 | Weak dominance strengthens to usual dominance on the power sets. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
β’ (π βΌ* π β π« π βΌ π« π) | ||
Theorem | canthwdom 9449 | Cantor's Theorem, stated using weak dominance (this is actually a stronger statement than canth2 9008, equivalent to canth 7303). (Contributed by Mario Carneiro, 15-May-2015.) |
β’ Β¬ π« π΄ βΌ* π΄ | ||
Theorem | wdom2d 9450* | Deduce weak dominance from an implicit onto function (stated in a way which avoids ax-rep 5241). (Contributed by Stefan O'Rear, 13-Feb-2015.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ ((π β§ π₯ β π΄) β βπ¦ β π΅ π₯ = π) β β’ (π β π΄ βΌ* π΅) | ||
Theorem | wdomd 9451* | Deduce weak dominance from an implicit onto function. (Contributed by Stefan O'Rear, 13-Feb-2015.) |
β’ (π β π΅ β π) & β’ ((π β§ π₯ β π΄) β βπ¦ β π΅ π₯ = π) β β’ (π β π΄ βΌ* π΅) | ||
Theorem | brwdom3 9452* | Condition for weak dominance with a condition reminiscent of wdomd 9451. (Contributed by Stefan O'Rear, 13-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.) |
β’ ((π β π β§ π β π) β (π βΌ* π β βπβπ₯ β π βπ¦ β π π₯ = (πβπ¦))) | ||
Theorem | brwdom3i 9453* | Weak dominance implies existence of a covering function. (Contributed by Stefan O'Rear, 13-Feb-2015.) |
β’ (π βΌ* π β βπβπ₯ β π βπ¦ β π π₯ = (πβπ¦)) | ||
Theorem | unwdomg 9454 | Weak dominance of a (disjoint) union. (Contributed by Stefan O'Rear, 13-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.) |
β’ ((π΄ βΌ* π΅ β§ πΆ βΌ* π· β§ (π΅ β© π·) = β ) β (π΄ βͺ πΆ) βΌ* (π΅ βͺ π·)) | ||
Theorem | xpwdomg 9455 | Weak dominance of a Cartesian product. (Contributed by Stefan O'Rear, 13-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.) |
β’ ((π΄ βΌ* π΅ β§ πΆ βΌ* π·) β (π΄ Γ πΆ) βΌ* (π΅ Γ π·)) | ||
Theorem | wdomima2g 9456 | A set is weakly dominant over its image under any function. This version of wdomimag 9457 is stated so as to avoid ax-rep 5241. (Contributed by Mario Carneiro, 25-Jun-2015.) |
β’ ((Fun πΉ β§ π΄ β π β§ (πΉ β π΄) β π) β (πΉ β π΄) βΌ* π΄) | ||
Theorem | wdomimag 9457 | A set is weakly dominant over its image under any function. (Contributed by Stefan O'Rear, 14-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.) |
β’ ((Fun πΉ β§ π΄ β π) β (πΉ β π΄) βΌ* π΄) | ||
Theorem | unxpwdom2 9458 | Lemma for unxpwdom 9459. (Contributed by Mario Carneiro, 15-May-2015.) |
β’ ((π΄ Γ π΄) β (π΅ βͺ πΆ) β (π΄ βΌ* π΅ β¨ π΄ βΌ πΆ)) | ||
Theorem | unxpwdom 9459 | If a Cartesian product is dominated by a union, then the base set is either weakly dominated by one factor of the union or dominated by the other. Extracted from Lemma 2.3 of [KanamoriPincus] p. 420. (Contributed by Mario Carneiro, 15-May-2015.) |
β’ ((π΄ Γ π΄) βΌ (π΅ βͺ πΆ) β (π΄ βΌ* π΅ β¨ π΄ βΌ πΆ)) | ||
Theorem | ixpiunwdom 9460* | Describe an onto function from the indexed cartesian product to the indexed union. Together with ixpssmapg 8800 this shows that βͺ π₯ β π΄π΅ and Xπ₯ β π΄π΅ have closely linked cardinalities. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ ((π΄ β π β§ βͺ π₯ β π΄ π΅ β π β§ Xπ₯ β π΄ π΅ β β ) β βͺ π₯ β π΄ π΅ βΌ* (Xπ₯ β π΄ π΅ Γ π΄)) | ||
Theorem | harwdom 9461 | The value of the Hartogs function at a set π is weakly dominated by π« (π Γ π). This follows from a more precise analysis of the bound used in hartogs 9414 to prove that (harβπ) is an ordinal. (Contributed by Mario Carneiro, 15-May-2015.) |
β’ (π β π β (harβπ) βΌ* π« (π Γ π)) | ||
Axiom | ax-reg 9462* | Axiom of Regularity. An axiom of Zermelo-Fraenkel set theory. Also called the Axiom of Foundation. A rather non-intuitive axiom that denies more than it asserts, it states (in the form of zfreg 9465) that every nonempty set contains a set disjoint from itself. One consequence is that it denies the existence of a set containing itself (elirrv 9466). A stronger version that works for proper classes is proved as zfregs 9602. (Contributed by NM, 14-Aug-1993.) |
β’ (βπ¦ π¦ β π₯ β βπ¦(π¦ β π₯ β§ βπ§(π§ β π¦ β Β¬ π§ β π₯))) | ||
Theorem | axreg2 9463* | Axiom of Regularity expressed more compactly. (Contributed by NM, 14-Aug-2003.) |
β’ (π₯ β π¦ β βπ₯(π₯ β π¦ β§ βπ§(π§ β π₯ β Β¬ π§ β π¦))) | ||
Theorem | zfregcl 9464* | The Axiom of Regularity with class variables. (Contributed by NM, 5-Aug-1994.) Replace sethood hypothesis with sethood antecedent. (Revised by BJ, 27-Apr-2021.) |
β’ (π΄ β π β (βπ₯ π₯ β π΄ β βπ₯ β π΄ βπ¦ β π₯ Β¬ π¦ β π΄)) | ||
Theorem | zfreg 9465* | The Axiom of Regularity using abbreviations. Axiom 6 of [TakeutiZaring] p. 21. This is called the "weak form". Axiom Reg of [BellMachover] p. 480. There is also a "strong form", not requiring that π΄ be a set, that can be proved with more difficulty (see zfregs 9602). (Contributed by NM, 26-Nov-1995.) Replace sethood hypothesis with sethood antecedent. (Revised by BJ, 27-Apr-2021.) |
β’ ((π΄ β π β§ π΄ β β ) β βπ₯ β π΄ (π₯ β© π΄) = β ) | ||
Theorem | elirrv 9466 | The membership relation is irreflexive: no set is a member of itself. Theorem 105 of [Suppes] p. 54. (This is trivial to prove from zfregfr 9475 and efrirr 5612, but this proof is direct from the Axiom of Regularity.) (Contributed by NM, 19-Aug-1993.) |
β’ Β¬ π₯ β π₯ | ||
Theorem | elirr 9467 | No class is a member of itself. Exercise 6 of [TakeutiZaring] p. 22. (Contributed by NM, 7-Aug-1994.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
β’ Β¬ π΄ β π΄ | ||
Theorem | elneq 9468 | A class is not equal to any of its elements. (Contributed by AV, 14-Jun-2022.) |
β’ (π΄ β π΅ β π΄ β π΅) | ||
Theorem | nelaneq 9469 | A class is not an element of and equal to a class at the same time. Variant of elneq 9468 analogously to elnotel 9480 and en2lp 9476. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 18-Jun-2022.) |
β’ Β¬ (π΄ β π΅ β§ π΄ = π΅) | ||
Theorem | epinid0 9470 | The membership relation and the identity relation are disjoint. Variable-free version of nelaneq 9469. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 18-Jun-2022.) |
β’ ( E β© I ) = β | ||
Theorem | sucprcreg 9471 | A class is equal to its successor iff it is a proper class (assuming the Axiom of Regularity). (Contributed by NM, 9-Jul-2004.) (Proof shortened by BJ, 16-Apr-2019.) |
β’ (Β¬ π΄ β V β suc π΄ = π΄) | ||
Theorem | ruv 9472 | The Russell class is equal to the universe V. Exercise 5 of [TakeutiZaring] p. 22. (Contributed by Alan Sare, 4-Oct-2008.) |
β’ {π₯ β£ π₯ β π₯} = V | ||
Theorem | ruALT 9473 | Alternate proof of ru 3737, simplified using (indirectly) the Axiom of Regularity ax-reg 9462. (Contributed by Alan Sare, 4-Oct-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ {π₯ β£ π₯ β π₯} β V | ||
Theorem | disjcsn 9474 | A class is disjoint from its singleton. A consequence of regularity. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Revised by BJ, 4-Apr-2019.) |
β’ (π΄ β© {π΄}) = β | ||
Theorem | zfregfr 9475 | The membership relation is well-founded on any class. (Contributed by NM, 26-Nov-1995.) |
β’ E Fr π΄ | ||
Theorem | en2lp 9476 | No class has 2-cycle membership loops. Theorem 7X(b) of [Enderton] p. 206. (Contributed by NM, 16-Oct-1996.) (Revised by Mario Carneiro, 25-Jun-2015.) |
β’ Β¬ (π΄ β π΅ β§ π΅ β π΄) | ||
Theorem | elnanel 9477 | Two classes are not elements of each other simultaneously. This is just a rewriting of en2lp 9476 and serves as an example in the context of Godel codes, see elnanelprv 33784. (Contributed by AV, 5-Nov-2023.) (New usage is discouraged.) |
β’ (π΄ β π΅ βΌ π΅ β π΄) | ||
Theorem | cnvepnep 9478 | The membership (epsilon) relation and its converse are disjoint, i.e., E is an asymmetric relation. Variable-free version of en2lp 9476. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 19-Jun-2022.) |
β’ (β‘ E β© E ) = β | ||
Theorem | epnsym 9479 | The membership (epsilon) relation is not symmetric. (Contributed by AV, 18-Jun-2022.) |
β’ β‘ E β E | ||
Theorem | elnotel 9480 | A class cannot be an element of one of its elements. (Contributed by AV, 14-Jun-2022.) |
β’ (π΄ β π΅ β Β¬ π΅ β π΄) | ||
Theorem | elnel 9481 | A class cannot be an element of one of its elements. (Contributed by AV, 14-Jun-2022.) |
β’ (π΄ β π΅ β π΅ β π΄) | ||
Theorem | en3lplem1 9482* | Lemma for en3lp 9484. (Contributed by Alan Sare, 28-Oct-2011.) |
β’ ((π΄ β π΅ β§ π΅ β πΆ β§ πΆ β π΄) β (π₯ = π΄ β (π₯ β© {π΄, π΅, πΆ}) β β )) | ||
Theorem | en3lplem2 9483* | Lemma for en3lp 9484. (Contributed by Alan Sare, 28-Oct-2011.) |
β’ ((π΄ β π΅ β§ π΅ β πΆ β§ πΆ β π΄) β (π₯ β {π΄, π΅, πΆ} β (π₯ β© {π΄, π΅, πΆ}) β β )) | ||
Theorem | en3lp 9484 | No class has 3-cycle membership loops. This proof was automatically generated from the virtual deduction proof en3lpVD 42860 using a translation program. (Contributed by Alan Sare, 24-Oct-2011.) |
β’ Β¬ (π΄ β π΅ β§ π΅ β πΆ β§ πΆ β π΄) | ||
Theorem | preleqg 9485 | Equality of two unordered pairs when one member of each pair contains the other member. Closed form of preleq 9486. (Contributed by AV, 15-Jun-2022.) |
β’ (((π΄ β π΅ β§ π΅ β π β§ πΆ β π·) β§ {π΄, π΅} = {πΆ, π·}) β (π΄ = πΆ β§ π΅ = π·)) | ||
Theorem | preleq 9486 | Equality of two unordered pairs when one member of each pair contains the other member. (Contributed by NM, 16-Oct-1996.) (Revised by AV, 15-Jun-2022.) |
β’ π΅ β V β β’ (((π΄ β π΅ β§ πΆ β π·) β§ {π΄, π΅} = {πΆ, π·}) β (π΄ = πΆ β§ π΅ = π·)) | ||
Theorem | preleqALT 9487 | Alternate proof of preleq 9486, not based on preleqg 9485: Equality of two unordered pairs when one member of each pair contains the other member. (Contributed by NM, 16-Oct-1996.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π΅ β V & β’ π· β V β β’ (((π΄ β π΅ β§ πΆ β π·) β§ {π΄, π΅} = {πΆ, π·}) β (π΄ = πΆ β§ π΅ = π·)) | ||
Theorem | opthreg 9488 | Theorem for alternate representation of ordered pairs, requiring the Axiom of Regularity ax-reg 9462 (via the preleq 9486 step). See df-op 4592 for a description of other ordered pair representations. Exercise 34 of [Enderton] p. 207. (Contributed by NM, 16-Oct-1996.) (Proof shortened by AV, 15-Jun-2022.) |
β’ π΄ β V & β’ π΅ β V & β’ πΆ β V & β’ π· β V β β’ ({π΄, {π΄, π΅}} = {πΆ, {πΆ, π·}} β (π΄ = πΆ β§ π΅ = π·)) | ||
Theorem | suc11reg 9489 | The successor operation behaves like a one-to-one function (assuming the Axiom of Regularity). Exercise 35 of [Enderton] p. 208 and its converse. (Contributed by NM, 25-Oct-2003.) |
β’ (suc π΄ = suc π΅ β π΄ = π΅) | ||
Theorem | dford2 9490* | Assuming ax-reg 9462, an ordinal is a transitive class on which inclusion satisfies trichotomy. (Contributed by Scott Fenton, 27-Oct-2010.) |
β’ (Ord π΄ β (Tr π΄ β§ βπ₯ β π΄ βπ¦ β π΄ (π₯ β π¦ β¨ π₯ = π¦ β¨ π¦ β π₯))) | ||
Theorem | inf0 9491* | Existence of Ο implies our axiom of infinity ax-inf 9508. The proof shows that the especially contrived class "ran (rec((π£ β V β¦ suc π£), π₯) βΎ Ο) " exists, is a subset of its union, and contains a given set π₯ (and thus is nonempty). Thus, it provides an example demonstrating that a set π¦ exists with the necessary properties demanded by ax-inf 9508. (Contributed by NM, 15-Oct-1996.) Revised to closed form. (Revised by BJ, 20-May-2024.) |
β’ (Ο β π β βπ¦(π₯ β π¦ β§ βπ§(π§ β π¦ β βπ€(π§ β π€ β§ π€ β π¦)))) | ||
Theorem | inf1 9492 | Variation of Axiom of Infinity (using zfinf 9509 as a hypothesis). Axiom of Infinity in [FreydScedrov] p. 283. (Contributed by NM, 14-Oct-1996.) (Revised by David Abernethy, 1-Oct-2013.) |
β’ βπ₯(π¦ β π₯ β§ βπ¦(π¦ β π₯ β βπ§(π¦ β π§ β§ π§ β π₯))) β β’ βπ₯(π₯ β β β§ βπ¦(π¦ β π₯ β βπ§(π¦ β π§ β§ π§ β π₯))) | ||
Theorem | inf2 9493* | Variation of Axiom of Infinity. There exists a nonempty set that is a subset of its union (using zfinf 9509 as a hypothesis). Abbreviated version of the Axiom of Infinity in [FreydScedrov] p. 283. (Contributed by NM, 28-Oct-1996.) |
β’ βπ₯(π¦ β π₯ β§ βπ¦(π¦ β π₯ β βπ§(π¦ β π§ β§ π§ β π₯))) β β’ βπ₯(π₯ β β β§ π₯ β βͺ π₯) | ||
Theorem | inf3lema 9494* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9505 for detailed description. (Contributed by NM, 28-Oct-1996.) |
β’ πΊ = (π¦ β V β¦ {π€ β π₯ β£ (π€ β© π₯) β π¦}) & β’ πΉ = (rec(πΊ, β ) βΎ Ο) & β’ π΄ β V & β’ π΅ β V β β’ (π΄ β (πΊβπ΅) β (π΄ β π₯ β§ (π΄ β© π₯) β π΅)) | ||
Theorem | inf3lemb 9495* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9505 for detailed description. (Contributed by NM, 28-Oct-1996.) |
β’ πΊ = (π¦ β V β¦ {π€ β π₯ β£ (π€ β© π₯) β π¦}) & β’ πΉ = (rec(πΊ, β ) βΎ Ο) & β’ π΄ β V & β’ π΅ β V β β’ (πΉββ ) = β | ||
Theorem | inf3lemc 9496* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9505 for detailed description. (Contributed by NM, 28-Oct-1996.) |
β’ πΊ = (π¦ β V β¦ {π€ β π₯ β£ (π€ β© π₯) β π¦}) & β’ πΉ = (rec(πΊ, β ) βΎ Ο) & β’ π΄ β V & β’ π΅ β V β β’ (π΄ β Ο β (πΉβsuc π΄) = (πΊβ(πΉβπ΄))) | ||
Theorem | inf3lemd 9497* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9505 for detailed description. (Contributed by NM, 28-Oct-1996.) |
β’ πΊ = (π¦ β V β¦ {π€ β π₯ β£ (π€ β© π₯) β π¦}) & β’ πΉ = (rec(πΊ, β ) βΎ Ο) & β’ π΄ β V & β’ π΅ β V β β’ (π΄ β Ο β (πΉβπ΄) β π₯) | ||
Theorem | inf3lem1 9498* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9505 for detailed description. (Contributed by NM, 28-Oct-1996.) |
β’ πΊ = (π¦ β V β¦ {π€ β π₯ β£ (π€ β© π₯) β π¦}) & β’ πΉ = (rec(πΊ, β ) βΎ Ο) & β’ π΄ β V & β’ π΅ β V β β’ (π΄ β Ο β (πΉβπ΄) β (πΉβsuc π΄)) | ||
Theorem | inf3lem2 9499* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9505 for detailed description. (Contributed by NM, 28-Oct-1996.) |
β’ πΊ = (π¦ β V β¦ {π€ β π₯ β£ (π€ β© π₯) β π¦}) & β’ πΉ = (rec(πΊ, β ) βΎ Ο) & β’ π΄ β V & β’ π΅ β V β β’ ((π₯ β β β§ π₯ β βͺ π₯) β (π΄ β Ο β (πΉβπ΄) β π₯)) | ||
Theorem | inf3lem3 9500* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9505 for detailed description. In the proof, we invoke the Axiom of Regularity in the form of zfreg 9465. (Contributed by NM, 29-Oct-1996.) |
β’ πΊ = (π¦ β V β¦ {π€ β π₯ β£ (π€ β© π₯) β π¦}) & β’ πΉ = (rec(πΊ, β ) βΎ Ο) & β’ π΄ β V & β’ π΅ β V β β’ ((π₯ β β β§ π₯ β βͺ π₯) β (π΄ β Ο β (πΉβπ΄) β (πΉβsuc π΄))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |