![]() |
Metamath
Proof Explorer Theorem List (p. 96 of 479) | < 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: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | inf00 9501 | The infimum regarding an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.) |
β’ inf(π΅, β , π ) = β | ||
Theorem | infempty 9502* | The infimum of an empty set under a base set which has a unique greatest element is the greatest element of the base set. (Contributed by AV, 4-Sep-2020.) |
β’ ((π Or π΄ β§ (π β π΄ β§ βπ¦ β π΄ Β¬ ππ π¦) β§ β!π₯ β π΄ βπ¦ β π΄ Β¬ π₯π π¦) β inf(β , π΄, π ) = π) | ||
Theorem | infiso 9503* | Image of an infimum under an isomorphism. (Contributed by AV, 4-Sep-2020.) |
β’ (π β πΉ Isom π , π (π΄, π΅)) & β’ (π β πΆ β π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β πΆ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β πΆ π§π π¦))) & β’ (π β π Or π΄) β β’ (π β inf((πΉ β πΆ), π΅, π) = (πΉβinf(πΆ, π΄, π ))) | ||
Syntax | coi 9504 | Extend class definition to include the canonical order isomorphism to an ordinal. |
class OrdIso(π , π΄) | ||
Definition | df-oi 9505* | Define the canonical order isomorphism from the well-order π on π΄ to an ordinal. (Contributed by Mario Carneiro, 23-May-2015.) |
β’ OrdIso(π , π΄) = if((π We π΄ β§ π Se π΄), (recs((β β V β¦ (β©π£ β {π€ β π΄ β£ βπ β ran β ππ π€}βπ’ β {π€ β π΄ β£ βπ β ran β ππ π€} Β¬ π’π π£))) βΎ {π₯ β On β£ βπ‘ β π΄ βπ§ β (recs((β β V β¦ (β©π£ β {π€ β π΄ β£ βπ β ran β ππ π€}βπ’ β {π€ β π΄ β£ βπ β ran β ππ π€} Β¬ π’π π£))) β π₯)π§π π‘}), β ) | ||
Theorem | dfoi 9506* | Rewrite df-oi 9505 with abbreviations. (Contributed by Mario Carneiro, 24-Jun-2015.) |
β’ πΆ = {π€ β π΄ β£ βπ β ran β ππ π€} & β’ πΊ = (β β V β¦ (β©π£ β πΆ βπ’ β πΆ Β¬ π’π π£)) & β’ πΉ = recs(πΊ) β β’ OrdIso(π , π΄) = if((π We π΄ β§ π Se π΄), (πΉ βΎ {π₯ β On β£ βπ‘ β π΄ βπ§ β (πΉ β π₯)π§π π‘}), β ) | ||
Theorem | oieq1 9507 | Equality theorem for ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015.) |
β’ (π = π β OrdIso(π , π΄) = OrdIso(π, π΄)) | ||
Theorem | oieq2 9508 | Equality theorem for ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015.) |
β’ (π΄ = π΅ β OrdIso(π , π΄) = OrdIso(π , π΅)) | ||
Theorem | nfoi 9509 | Hypothesis builder for ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015.) (Revised by Mario Carneiro, 15-Oct-2016.) |
β’ β²π₯π & β’ β²π₯π΄ β β’ β²π₯OrdIso(π , π΄) | ||
Theorem | ordiso2 9510 | Generalize ordiso 9511 to proper classes. (Contributed by Mario Carneiro, 24-Jun-2015.) |
β’ ((πΉ Isom E , E (π΄, π΅) β§ Ord π΄ β§ Ord π΅) β π΄ = π΅) | ||
Theorem | ordiso 9511* | Order-isomorphic ordinal numbers are equal. (Contributed by Jeff Hankins, 16-Oct-2009.) (Proof shortened by Mario Carneiro, 24-Jun-2015.) |
β’ ((π΄ β On β§ π΅ β On) β (π΄ = π΅ β βπ π Isom E , E (π΄, π΅))) | ||
Theorem | ordtypecbv 9512* | Lemma for ordtype 9527. (Contributed by Mario Carneiro, 26-Jun-2015.) |
β’ πΉ = recs(πΊ) & β’ πΆ = {π€ β π΄ β£ βπ β ran β ππ π€} & β’ πΊ = (β β V β¦ (β©π£ β πΆ βπ’ β πΆ Β¬ π’π π£)) β β’ recs((π β V β¦ (β©π β {π¦ β π΄ β£ βπ β ran π ππ π¦}βπ β {π¦ β π΄ β£ βπ β ran π ππ π¦} Β¬ ππ π ))) = πΉ | ||
Theorem | ordtypelem1 9513* | Lemma for ordtype 9527. (Contributed by Mario Carneiro, 24-Jun-2015.) |
β’ πΉ = recs(πΊ) & β’ πΆ = {π€ β π΄ β£ βπ β ran β ππ π€} & β’ πΊ = (β β V β¦ (β©π£ β πΆ βπ’ β πΆ Β¬ π’π π£)) & β’ π = {π₯ β On β£ βπ‘ β π΄ βπ§ β (πΉ β π₯)π§π π‘} & β’ π = OrdIso(π , π΄) & β’ (π β π We π΄) & β’ (π β π Se π΄) β β’ (π β π = (πΉ βΎ π)) | ||
Theorem | ordtypelem2 9514* | Lemma for ordtype 9527. (Contributed by Mario Carneiro, 24-Jun-2015.) |
β’ πΉ = recs(πΊ) & β’ πΆ = {π€ β π΄ β£ βπ β ran β ππ π€} & β’ πΊ = (β β V β¦ (β©π£ β πΆ βπ’ β πΆ Β¬ π’π π£)) & β’ π = {π₯ β On β£ βπ‘ β π΄ βπ§ β (πΉ β π₯)π§π π‘} & β’ π = OrdIso(π , π΄) & β’ (π β π We π΄) & β’ (π β π Se π΄) β β’ (π β Ord π) | ||
Theorem | ordtypelem3 9515* | Lemma for ordtype 9527. (Contributed by Mario Carneiro, 24-Jun-2015.) |
β’ πΉ = recs(πΊ) & β’ πΆ = {π€ β π΄ β£ βπ β ran β ππ π€} & β’ πΊ = (β β V β¦ (β©π£ β πΆ βπ’ β πΆ Β¬ π’π π£)) & β’ π = {π₯ β On β£ βπ‘ β π΄ βπ§ β (πΉ β π₯)π§π π‘} & β’ π = OrdIso(π , π΄) & β’ (π β π We π΄) & β’ (π β π Se π΄) β β’ ((π β§ π β (π β© dom πΉ)) β (πΉβπ) β {π£ β {π€ β π΄ β£ βπ β (πΉ β π)ππ π€} β£ βπ’ β {π€ β π΄ β£ βπ β (πΉ β π)ππ π€} Β¬ π’π π£}) | ||
Theorem | ordtypelem4 9516* | Lemma for ordtype 9527. (Contributed by Mario Carneiro, 24-Jun-2015.) |
β’ πΉ = recs(πΊ) & β’ πΆ = {π€ β π΄ β£ βπ β ran β ππ π€} & β’ πΊ = (β β V β¦ (β©π£ β πΆ βπ’ β πΆ Β¬ π’π π£)) & β’ π = {π₯ β On β£ βπ‘ β π΄ βπ§ β (πΉ β π₯)π§π π‘} & β’ π = OrdIso(π , π΄) & β’ (π β π We π΄) & β’ (π β π Se π΄) β β’ (π β π:(π β© dom πΉ)βΆπ΄) | ||
Theorem | ordtypelem5 9517* | Lemma for ordtype 9527. (Contributed by Mario Carneiro, 25-Jun-2015.) |
β’ πΉ = recs(πΊ) & β’ πΆ = {π€ β π΄ β£ βπ β ran β ππ π€} & β’ πΊ = (β β V β¦ (β©π£ β πΆ βπ’ β πΆ Β¬ π’π π£)) & β’ π = {π₯ β On β£ βπ‘ β π΄ βπ§ β (πΉ β π₯)π§π π‘} & β’ π = OrdIso(π , π΄) & β’ (π β π We π΄) & β’ (π β π Se π΄) β β’ (π β (Ord dom π β§ π:dom πβΆπ΄)) | ||
Theorem | ordtypelem6 9518* | Lemma for ordtype 9527. (Contributed by Mario Carneiro, 24-Jun-2015.) |
β’ πΉ = recs(πΊ) & β’ πΆ = {π€ β π΄ β£ βπ β ran β ππ π€} & β’ πΊ = (β β V β¦ (β©π£ β πΆ βπ’ β πΆ Β¬ π’π π£)) & β’ π = {π₯ β On β£ βπ‘ β π΄ βπ§ β (πΉ β π₯)π§π π‘} & β’ π = OrdIso(π , π΄) & β’ (π β π We π΄) & β’ (π β π Se π΄) β β’ ((π β§ π β dom π) β (π β π β (πβπ)π (πβπ))) | ||
Theorem | ordtypelem7 9519* | Lemma for ordtype 9527. ran π is an initial segment of π΄ under the well-order π . (Contributed by Mario Carneiro, 25-Jun-2015.) |
β’ πΉ = recs(πΊ) & β’ πΆ = {π€ β π΄ β£ βπ β ran β ππ π€} & β’ πΊ = (β β V β¦ (β©π£ β πΆ βπ’ β πΆ Β¬ π’π π£)) & β’ π = {π₯ β On β£ βπ‘ β π΄ βπ§ β (πΉ β π₯)π§π π‘} & β’ π = OrdIso(π , π΄) & β’ (π β π We π΄) & β’ (π β π Se π΄) β β’ (((π β§ π β π΄) β§ π β dom π) β ((πβπ)π π β¨ π β ran π)) | ||
Theorem | ordtypelem8 9520* | Lemma for ordtype 9527. (Contributed by Mario Carneiro, 25-Jun-2015.) |
β’ πΉ = recs(πΊ) & β’ πΆ = {π€ β π΄ β£ βπ β ran β ππ π€} & β’ πΊ = (β β V β¦ (β©π£ β πΆ βπ’ β πΆ Β¬ π’π π£)) & β’ π = {π₯ β On β£ βπ‘ β π΄ βπ§ β (πΉ β π₯)π§π π‘} & β’ π = OrdIso(π , π΄) & β’ (π β π We π΄) & β’ (π β π Se π΄) β β’ (π β π Isom E , π (dom π, ran π)) | ||
Theorem | ordtypelem9 9521* | Lemma for ordtype 9527. Either the function OrdIso is an isomorphism onto all of π΄, or OrdIso is not a set, which by oif 9525 implies that either ran π β π΄ is a proper class or dom π = On. (Contributed by Mario Carneiro, 25-Jun-2015.) (Revised by AV, 28-Jul-2024.) |
β’ πΉ = recs(πΊ) & β’ πΆ = {π€ β π΄ β£ βπ β ran β ππ π€} & β’ πΊ = (β β V β¦ (β©π£ β πΆ βπ’ β πΆ Β¬ π’π π£)) & β’ π = {π₯ β On β£ βπ‘ β π΄ βπ§ β (πΉ β π₯)π§π π‘} & β’ π = OrdIso(π , π΄) & β’ (π β π We π΄) & β’ (π β π Se π΄) & β’ (π β π β π) β β’ (π β π Isom E , π (dom π, π΄)) | ||
Theorem | ordtypelem10 9522* | Lemma for ordtype 9527. Using ax-rep 5286, exclude the possibility that π is a proper class and does not enumerate all of π΄. (Contributed by Mario Carneiro, 25-Jun-2015.) |
β’ πΉ = recs(πΊ) & β’ πΆ = {π€ β π΄ β£ βπ β ran β ππ π€} & β’ πΊ = (β β V β¦ (β©π£ β πΆ βπ’ β πΆ Β¬ π’π π£)) & β’ π = {π₯ β On β£ βπ‘ β π΄ βπ§ β (πΉ β π₯)π§π π‘} & β’ π = OrdIso(π , π΄) & β’ (π β π We π΄) & β’ (π β π Se π΄) β β’ (π β π Isom E , π (dom π, π΄)) | ||
Theorem | oi0 9523 | Definition of the ordinal isomorphism when its arguments are not meaningful. (Contributed by Mario Carneiro, 25-Jun-2015.) |
β’ πΉ = OrdIso(π , π΄) β β’ (Β¬ (π We π΄ β§ π Se π΄) β πΉ = β ) | ||
Theorem | oicl 9524 | The order type of the well-order π on π΄ is an ordinal. (Contributed by Mario Carneiro, 23-May-2015.) (Revised by Mario Carneiro, 25-Jun-2015.) |
β’ πΉ = OrdIso(π , π΄) β β’ Ord dom πΉ | ||
Theorem | oif 9525 | The order isomorphism of the well-order π on π΄ is a function. (Contributed by Mario Carneiro, 23-May-2015.) |
β’ πΉ = OrdIso(π , π΄) β β’ πΉ:dom πΉβΆπ΄ | ||
Theorem | oiiso2 9526 | The order isomorphism of the well-order π on π΄ is an isomorphism onto ran π (which is a subset of π΄ by oif 9525). (Contributed by Mario Carneiro, 25-Jun-2015.) |
β’ πΉ = OrdIso(π , π΄) β β’ ((π We π΄ β§ π Se π΄) β πΉ Isom E , π (dom πΉ, ran πΉ)) | ||
Theorem | ordtype 9527 | 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 9528 | ran πΉ is an initial segment of π΄ under the well-order π . (Contributed by Mario Carneiro, 26-Jun-2015.) |
β’ πΉ = OrdIso(π , π΄) β β’ (((π We π΄ β§ π Se π΄) β§ (π β π΄ β§ π β dom πΉ)) β ((πΉβπ)π π β¨ π β ran πΉ)) | ||
Theorem | ordtype2 9529 | 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 9527 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 25-Jun-2015.) |
β’ πΉ = OrdIso(π , π΄) β β’ ((π We π΄ β§ π Se π΄ β§ πΉ β V) β πΉ Isom E , π (dom πΉ, π΄)) | ||
Theorem | oiexg 9530 | The order isomorphism on a set is a set. (Contributed by Mario Carneiro, 25-Jun-2015.) |
β’ πΉ = OrdIso(π , π΄) β β’ (π΄ β π β πΉ β V) | ||
Theorem | oion 9531 | 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 9532 | 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 9533 | 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 9534 | 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 9535 | 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 5286 (the second statement is trivial under ax-rep 5286). (Contributed by Mario Carneiro, 26-Jun-2015.) |
β’ πΉ = OrdIso( E , π΄) β β’ (π΄ β On β (Smo πΉ β§ ran πΉ = π΄)) | ||
Theorem | oiid 9536 | 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 9537* | Lemma for hartogs 9539. (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 9538* | Lemma for hartogs 9539. (Contributed by Mario Carneiro, 14-Jan-2013.) |
β’ πΉ = {β¨π, π¦β© β£ (((dom π β π΄ β§ ( I βΎ dom π) β π β§ π β (dom π Γ dom π)) β§ (π β I ) We dom π) β§ π¦ = dom OrdIso((π β I ), dom π))} & β’ π = {β¨π , π‘β© β£ βπ€ β π¦ βπ§ β π¦ ((π = (πβπ€) β§ π‘ = (πβπ§)) β§ π€ E π§)} β β’ (π΄ β π β {π₯ β On β£ π₯ βΌ π΄} β V) | ||
Theorem | hartogs 9539* | The class of ordinals dominated by a given set is an ordinal. A shorter (when taking into account lemmas hartogslem1 9537 and hartogslem2 9538) proof can be given using the axiom of choice, see ondomon 10558. As its label indicates, this result is used to justify the definition of the Hartogs function df-har 9552. (Contributed by Jeff Hankins, 22-Oct-2009.) (Revised by Mario Carneiro, 15-May-2015.) |
β’ (π΄ β π β {π₯ β On β£ π₯ βΌ π΄} β On) | ||
Theorem | wofib 9540 | 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 9541* | Value of the lexicographic order on a sequence space. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
β’ π = {β¨π₯, π¦β© β£ βπ§ β π΄ ((π₯βπ§)π(π¦βπ§) β§ βπ€ β π΄ (π€π π§ β (π₯βπ€) = (π¦βπ€)))} β β’ ((π β π β§ π β π) β (πππ β βπ β π΄ ((πβπ)π(πβπ) β§ βπ β π΄ (ππ π β (πβπ) = (πβπ))))) | ||
Theorem | wemaplem2 9542* | Lemma for wemapso 9546. Transitivity. (Contributed by Stefan O'Rear, 17-Jan-2015.) (Revised by AV, 21-Jul-2024.) |
β’ π = {β¨π₯, π¦β© β£ βπ§ β π΄ ((π₯βπ§)π(π¦βπ§) β§ βπ€ β π΄ (π€π π§ β (π₯βπ€) = (π¦βπ€)))} & β’ (π β π β (π΅ βm π΄)) & β’ (π β π β (π΅ βm π΄)) & β’ (π β π β (π΅ βm π΄)) & β’ (π β π Or π΄) & β’ (π β π Po π΅) & β’ (π β π β π΄) & β’ (π β (πβπ)π(πβπ)) & β’ (π β βπ β π΄ (ππ π β (πβπ) = (πβπ))) & β’ (π β π β π΄) & β’ (π β (πβπ)π(πβπ)) & β’ (π β βπ β π΄ (ππ π β (πβπ) = (πβπ))) β β’ (π β πππ) | ||
Theorem | wemaplem3 9543* | Lemma for wemapso 9546. Transitivity. (Contributed by Stefan O'Rear, 17-Jan-2015.) (Revised by AV, 21-Jul-2024.) |
β’ π = {β¨π₯, π¦β© β£ βπ§ β π΄ ((π₯βπ§)π(π¦βπ§) β§ βπ€ β π΄ (π€π π§ β (π₯βπ€) = (π¦βπ€)))} & β’ (π β π β (π΅ βm π΄)) & β’ (π β π β (π΅ βm π΄)) & β’ (π β π β (π΅ βm π΄)) & β’ (π β π Or π΄) & β’ (π β π Po π΅) & β’ (π β πππ) & β’ (π β πππ) β β’ (π β πππ) | ||
Theorem | wemappo 9544* |
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 9545* | Lemma for wemapso 9546. (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 9546* | 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 9547* | Lemma for wemapso2 9548. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 1-Jul-2019.) |
β’ π = {β¨π₯, π¦β© β£ βπ§ β π΄ ((π₯βπ§)π(π¦βπ§) β§ βπ€ β π΄ (π€π π§ β (π₯βπ€) = (π¦βπ€)))} & β’ π = {π₯ β (π΅ βm π΄) β£ π₯ finSupp π} β β’ (((π΄ β π β§ π Or π΄ β§ π Or π΅) β§ π β π) β π Or π) | ||
Theorem | wemapso2 9548* | An alternative to having a well-order on π in wemapso 9546 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 9549* | The alternate definition of the cardinal of a set given in cardval2 9986 always gives a set, and indeed an ordinal. (Contributed by Mario Carneiro, 14-Jan-2013.) |
β’ {π₯ β On β£ π₯ βΊ π΄} β On | ||
Theorem | card2inf 9550* | The alternate definition of the cardinal of a set given in cardval2 9986 has the curious property that for non-numerable sets (for which ndmfv 6927 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 9551 | Class symbol for the Hartogs function. |
class har | ||
Definition | df-har 9552* |
Define the Hartogs function as mapping a set to the class of ordinals it
dominates. That class is an ordinal by hartogs 9539, which is used in
harf 9553.
The Hartogs number of a set is the least ordinal not dominated by that set. Theorem harval2 9992 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 9993. 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 9935. 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 9553 | Functionality of the Hartogs function. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
β’ har:VβΆOn | ||
Theorem | harcl 9554 | 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 9555* | Function value of the Hartogs function. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
β’ (π β π β (harβπ) = {π¦ β On β£ π¦ βΌ π}) | ||
Theorem | elharval 9556 | The Hartogs number of a set contains exactly the ordinals that set dominates. Combined with harcl 9554, 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 9557 | 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 9558 | Weak ordering property of the Hartogs function. (Contributed by Stefan O'Rear, 14-Feb-2015.) |
β’ (π βΌ π β (harβπ) β (harβπ)) | ||
Syntax | cwdom 9559 | Class symbol for the weak dominance relation. |
class βΌ* | ||
Definition | df-wdom 9560* | 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 8941) implies weak dominance (over ZF). The principle asserting the converse is known as the partition principle and is independent of ZF. Theorem fodom 10518 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 9561 | Weak dominance is a relation. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
β’ Rel βΌ* | ||
Theorem | brwdom 9562* | Property of weak dominance (definitional form). (Contributed by Stefan O'Rear, 11-Feb-2015.) |
β’ (π β π β (π βΌ* π β (π = β β¨ βπ§ π§:πβontoβπ))) | ||
Theorem | brwdomi 9563* | Property of weak dominance, forward direction only. (Contributed by Mario Carneiro, 5-May-2015.) |
β’ (π βΌ* π β (π = β β¨ βπ§ π§:πβontoβπ)) | ||
Theorem | brwdomn0 9564* | Weak dominance over nonempty sets. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
β’ (π β β β (π βΌ* π β βπ§ π§:πβontoβπ)) | ||
Theorem | 0wdom 9565 | Any set weakly dominates the empty set. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
β’ (π β π β β βΌ* π) | ||
Theorem | fowdom 9566 | An onto function implies weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
β’ ((πΉ β π β§ πΉ:πβontoβπ) β π βΌ* π) | ||
Theorem | wdomref 9567 | Reflexivity of weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
β’ (π β π β π βΌ* π) | ||
Theorem | brwdom2 9568* | 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 9569 | Weak dominance is implied by dominance in the usual sense. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
β’ (π βΌ π β π βΌ* π) | ||
Theorem | wdomtr 9570 | Transitivity of weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
β’ ((π βΌ* π β§ π βΌ* π) β π βΌ* π) | ||
Theorem | wdomen1 9571 | Equality-like theorem for equinumerosity and weak dominance. (Contributed by Mario Carneiro, 18-May-2015.) |
β’ (π΄ β π΅ β (π΄ βΌ* πΆ β π΅ βΌ* πΆ)) | ||
Theorem | wdomen2 9572 | Equality-like theorem for equinumerosity and weak dominance. (Contributed by Mario Carneiro, 18-May-2015.) |
β’ (π΄ β π΅ β (πΆ βΌ* π΄ β πΆ βΌ* π΅)) | ||
Theorem | wdompwdom 9573 | 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 9574 | Cantor's Theorem, stated using weak dominance (this is actually a stronger statement than canth2 9130, equivalent to canth 7362). (Contributed by Mario Carneiro, 15-May-2015.) |
β’ Β¬ π« π΄ βΌ* π΄ | ||
Theorem | wdom2d 9575* | Deduce weak dominance from an implicit onto function (stated in a way which avoids ax-rep 5286). (Contributed by Stefan O'Rear, 13-Feb-2015.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ ((π β§ π₯ β π΄) β βπ¦ β π΅ π₯ = π) β β’ (π β π΄ βΌ* π΅) | ||
Theorem | wdomd 9576* | Deduce weak dominance from an implicit onto function. (Contributed by Stefan O'Rear, 13-Feb-2015.) |
β’ (π β π΅ β π) & β’ ((π β§ π₯ β π΄) β βπ¦ β π΅ π₯ = π) β β’ (π β π΄ βΌ* π΅) | ||
Theorem | brwdom3 9577* | Condition for weak dominance with a condition reminiscent of wdomd 9576. (Contributed by Stefan O'Rear, 13-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.) |
β’ ((π β π β§ π β π) β (π βΌ* π β βπβπ₯ β π βπ¦ β π π₯ = (πβπ¦))) | ||
Theorem | brwdom3i 9578* | Weak dominance implies existence of a covering function. (Contributed by Stefan O'Rear, 13-Feb-2015.) |
β’ (π βΌ* π β βπβπ₯ β π βπ¦ β π π₯ = (πβπ¦)) | ||
Theorem | unwdomg 9579 | Weak dominance of a (disjoint) union. (Contributed by Stefan O'Rear, 13-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.) |
β’ ((π΄ βΌ* π΅ β§ πΆ βΌ* π· β§ (π΅ β© π·) = β ) β (π΄ βͺ πΆ) βΌ* (π΅ βͺ π·)) | ||
Theorem | xpwdomg 9580 | Weak dominance of a Cartesian product. (Contributed by Stefan O'Rear, 13-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.) |
β’ ((π΄ βΌ* π΅ β§ πΆ βΌ* π·) β (π΄ Γ πΆ) βΌ* (π΅ Γ π·)) | ||
Theorem | wdomima2g 9581 | A set is weakly dominant over its image under any function. This version of wdomimag 9582 is stated so as to avoid ax-rep 5286. (Contributed by Mario Carneiro, 25-Jun-2015.) |
β’ ((Fun πΉ β§ π΄ β π β§ (πΉ β π΄) β π) β (πΉ β π΄) βΌ* π΄) | ||
Theorem | wdomimag 9582 | 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 9583 | Lemma for unxpwdom 9584. (Contributed by Mario Carneiro, 15-May-2015.) |
β’ ((π΄ Γ π΄) β (π΅ βͺ πΆ) β (π΄ βΌ* π΅ β¨ π΄ βΌ πΆ)) | ||
Theorem | unxpwdom 9584 | 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 9585* | Describe an onto function from the indexed cartesian product to the indexed union. Together with ixpssmapg 8922 this shows that βͺ π₯ β π΄π΅ and Xπ₯ β π΄π΅ have closely linked cardinalities. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ ((π΄ β π β§ βͺ π₯ β π΄ π΅ β π β§ Xπ₯ β π΄ π΅ β β ) β βͺ π₯ β π΄ π΅ βΌ* (Xπ₯ β π΄ π΅ Γ π΄)) | ||
Theorem | harwdom 9586 | 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 9539 to prove that (harβπ) is an ordinal. (Contributed by Mario Carneiro, 15-May-2015.) |
β’ (π β π β (harβπ) βΌ* π« (π Γ π)) | ||
Axiom | ax-reg 9587* | 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 9590) that every nonempty set contains a set disjoint from itself. One consequence is that it denies the existence of a set containing itself (elirrv 9591). A stronger version that works for proper classes is proved as zfregs 9727. (Contributed by NM, 14-Aug-1993.) |
β’ (βπ¦ π¦ β π₯ β βπ¦(π¦ β π₯ β§ βπ§(π§ β π¦ β Β¬ π§ β π₯))) | ||
Theorem | axreg2 9588* | Axiom of Regularity expressed more compactly. (Contributed by NM, 14-Aug-2003.) |
β’ (π₯ β π¦ β βπ₯(π₯ β π¦ β§ βπ§(π§ β π₯ β Β¬ π§ β π¦))) | ||
Theorem | zfregcl 9589* | 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 9590* | 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 9727). (Contributed by NM, 26-Nov-1995.) Replace sethood hypothesis with sethood antecedent. (Revised by BJ, 27-Apr-2021.) |
β’ ((π΄ β π β§ π΄ β β ) β βπ₯ β π΄ (π₯ β© π΄) = β ) | ||
Theorem | elirrv 9591 | 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 9600 and efrirr 5658, but this proof is direct from the Axiom of Regularity.) (Contributed by NM, 19-Aug-1993.) |
β’ Β¬ π₯ β π₯ | ||
Theorem | elirr 9592 | No class is a member of itself. Exercise 6 of [TakeutiZaring] p. 22. Theorem 1.9(i) of [Schloeder] p. 1. (Contributed by NM, 7-Aug-1994.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
β’ Β¬ π΄ β π΄ | ||
Theorem | elneq 9593 | A class is not equal to any of its elements. (Contributed by AV, 14-Jun-2022.) |
β’ (π΄ β π΅ β π΄ β π΅) | ||
Theorem | nelaneq 9594 | A class is not an element of and equal to a class at the same time. Variant of elneq 9593 analogously to elnotel 9605 and en2lp 9601. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 18-Jun-2022.) |
β’ Β¬ (π΄ β π΅ β§ π΄ = π΅) | ||
Theorem | epinid0 9595 | The membership relation and the identity relation are disjoint. Variable-free version of nelaneq 9594. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 18-Jun-2022.) |
β’ ( E β© I ) = β | ||
Theorem | sucprcreg 9596 | 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 9597 | 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 9598 | Alternate proof of ru 3777, simplified using (indirectly) the Axiom of Regularity ax-reg 9587. (Contributed by Alan Sare, 4-Oct-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ {π₯ β£ π₯ β π₯} β V | ||
Theorem | disjcsn 9599 | 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 9600 | The membership relation is well-founded on any class. (Contributed by NM, 26-Nov-1995.) |
β’ E Fr π΄ |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |