Home | Metamath
Proof Explorer Theorem List (p. 106 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 | fpwwe2lem1 10501* | Lemma for fpwwe2 10513. (Contributed by Mario Carneiro, 15-May-2015.) |
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ [(β‘π β {π¦}) / π’](π’πΉ(π β© (π’ Γ π’))) = π¦))} β β’ π β (π« π΄ Γ π« (π΄ Γ π΄)) | ||
Theorem | fpwwe2lem2 10502* | Lemma for fpwwe2 10513. (Contributed by Mario Carneiro, 19-May-2015.) (Revised by AV, 20-Jul-2024.) |
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ [(β‘π β {π¦}) / π’](π’πΉ(π β© (π’ Γ π’))) = π¦))} & β’ (π β π΄ β π) β β’ (π β (πππ β ((π β π΄ β§ π β (π Γ π)) β§ (π We π β§ βπ¦ β π [(β‘π β {π¦}) / π’](π’πΉ(π β© (π’ Γ π’))) = π¦)))) | ||
Theorem | fpwwe2lem3 10503* | Lemma for fpwwe2 10513. (Contributed by Mario Carneiro, 19-May-2015.) (Revised by AV, 20-Jul-2024.) |
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ [(β‘π β {π¦}) / π’](π’πΉ(π β© (π’ Γ π’))) = π¦))} & β’ (π β π΄ β π) & β’ (π β πππ ) β β’ ((π β§ π΅ β π) β ((β‘π β {π΅})πΉ(π β© ((β‘π β {π΅}) Γ (β‘π β {π΅})))) = π΅) | ||
Theorem | fpwwe2lem4 10504* | Lemma for fpwwe2 10513. (Contributed by Mario Carneiro, 15-May-2015.) (Revised by AV, 20-Jul-2024.) |
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ [(β‘π β {π¦}) / π’](π’πΉ(π β© (π’ Γ π’))) = π¦))} & β’ (π β π΄ β π) & β’ ((π β§ (π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯)) β (π₯πΉπ) β π΄) β β’ ((π β§ (π β π΄ β§ π β (π Γ π) β§ π We π)) β (ππΉπ ) β π΄) | ||
Theorem | fpwwe2lem5 10505* | Lemma for fpwwe2 10513. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by AV, 20-Jul-2024.) |
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ [(β‘π β {π¦}) / π’](π’πΉ(π β© (π’ Γ π’))) = π¦))} & β’ (π β π΄ β π) & β’ ((π β§ (π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯)) β (π₯πΉπ) β π΄) & β’ (π β πππ ) & β’ (π β πππ) & β’ π = OrdIso(π , π) & β’ π = OrdIso(π, π) & β’ (π β π΅ β dom π) & β’ (π β π΅ β dom π) & β’ (π β (π βΎ π΅) = (π βΎ π΅)) β β’ ((π β§ πΆπ (πβπ΅)) β (πΆ β π β§ πΆ β π β§ (β‘πβπΆ) = (β‘πβπΆ))) | ||
Theorem | fpwwe2lem6 10506* | Lemma for fpwwe2 10513. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by AV, 20-Jul-2024.) |
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ [(β‘π β {π¦}) / π’](π’πΉ(π β© (π’ Γ π’))) = π¦))} & β’ (π β π΄ β π) & β’ ((π β§ (π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯)) β (π₯πΉπ) β π΄) & β’ (π β πππ ) & β’ (π β πππ) & β’ π = OrdIso(π , π) & β’ π = OrdIso(π, π) & β’ (π β π΅ β dom π) & β’ (π β π΅ β dom π) & β’ (π β (π βΎ π΅) = (π βΎ π΅)) β β’ ((π β§ πΆπ (πβπ΅)) β (πΆπ(πβπ΅) β§ (π·π (πβπ΅) β (πΆπ π· β πΆππ·)))) | ||
Theorem | fpwwe2lem7 10507* | Lemma for fpwwe2 10513. Show by induction that the two isometries π and π agree on their common domain. (Contributed by Mario Carneiro, 15-May-2015.) (Proof shortened by Peter Mazsa, 23-Sep-2022.) (Revised by AV, 20-Jul-2024.) |
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ [(β‘π β {π¦}) / π’](π’πΉ(π β© (π’ Γ π’))) = π¦))} & β’ (π β π΄ β π) & β’ ((π β§ (π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯)) β (π₯πΉπ) β π΄) & β’ (π β πππ ) & β’ (π β πππ) & β’ π = OrdIso(π , π) & β’ π = OrdIso(π, π) & β’ (π β dom π β dom π) β β’ (π β π = (π βΎ dom π)) | ||
Theorem | fpwwe2lem8 10508* | Lemma for fpwwe2 10513. Given two well-orders β¨π, π β© and β¨π, πβ© of parts of π΄, one is an initial segment of the other. (The π β π hypothesis is in order to break the symmetry of π and π.) (Contributed by Mario Carneiro, 15-May-2015.) (Proof shortened by Peter Mazsa, 23-Sep-2022.) (Revised by AV, 20-Jul-2024.) |
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ [(β‘π β {π¦}) / π’](π’πΉ(π β© (π’ Γ π’))) = π¦))} & β’ (π β π΄ β π) & β’ ((π β§ (π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯)) β (π₯πΉπ) β π΄) & β’ (π β πππ ) & β’ (π β πππ) & β’ π = OrdIso(π , π) & β’ π = OrdIso(π, π) & β’ (π β dom π β dom π) β β’ (π β (π β π β§ π = (π β© (π Γ π)))) | ||
Theorem | fpwwe2lem9 10509* | Lemma for fpwwe2 10513. Given two well-orders β¨π, π β© and β¨π, πβ© of parts of π΄, one is an initial segment of the other. (Contributed by Mario Carneiro, 15-May-2015.) (Revised by AV, 20-Jul-2024.) |
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ [(β‘π β {π¦}) / π’](π’πΉ(π β© (π’ Γ π’))) = π¦))} & β’ (π β π΄ β π) & β’ ((π β§ (π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯)) β (π₯πΉπ) β π΄) & β’ (π β πππ ) & β’ (π β πππ) β β’ (π β ((π β π β§ π = (π β© (π Γ π))) β¨ (π β π β§ π = (π β© (π Γ π))))) | ||
Theorem | fpwwe2lem10 10510* | Lemma for fpwwe2 10513. (Contributed by Mario Carneiro, 15-May-2015.) (Revised by AV, 20-Jul-2024.) |
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ [(β‘π β {π¦}) / π’](π’πΉ(π β© (π’ Γ π’))) = π¦))} & β’ (π β π΄ β π) & β’ ((π β§ (π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯)) β (π₯πΉπ) β π΄) & β’ π = βͺ dom π β β’ (π β π:dom πβΆπ« (π Γ π)) | ||
Theorem | fpwwe2lem11 10511* | Lemma for fpwwe2 10513. (Contributed by Mario Carneiro, 18-May-2015.) (Proof shortened by Peter Mazsa, 23-Sep-2022.) (Revised by AV, 20-Jul-2024.) |
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ [(β‘π β {π¦}) / π’](π’πΉ(π β© (π’ Γ π’))) = π¦))} & β’ (π β π΄ β π) & β’ ((π β§ (π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯)) β (π₯πΉπ) β π΄) & β’ π = βͺ dom π β β’ (π β π β dom π) | ||
Theorem | fpwwe2lem12 10512* | Lemma for fpwwe2 10513. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by AV, 20-Jul-2024.) |
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ [(β‘π β {π¦}) / π’](π’πΉ(π β© (π’ Γ π’))) = π¦))} & β’ (π β π΄ β π) & β’ ((π β§ (π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯)) β (π₯πΉπ) β π΄) & β’ π = βͺ dom π β β’ (π β (ππΉ(πβπ)) β π) | ||
Theorem | fpwwe2 10513* | Given any function πΉ from well-orderings of subsets of π΄ to π΄, there is a unique well-ordered subset β¨π, (πβπ)β© which "agrees" with πΉ in the sense that each initial segment maps to its upper bound, and such that the entire set maps to an element of the set (so that it cannot be extended without losing the well-ordering). This theorem can be used to prove dfac8a 9900. Theorem 1.1 of [KanamoriPincus] p. 415. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by AV, 20-Jul-2024.) |
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ [(β‘π β {π¦}) / π’](π’πΉ(π β© (π’ Γ π’))) = π¦))} & β’ (π β π΄ β π) & β’ ((π β§ (π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯)) β (π₯πΉπ) β π΄) & β’ π = βͺ dom π β β’ (π β ((πππ β§ (ππΉπ ) β π) β (π = π β§ π = (πβπ)))) | ||
Theorem | fpwwecbv 10514* | Lemma for fpwwe 10516. (Contributed by Mario Carneiro, 15-May-2015.) |
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ (πΉβ(β‘π β {π¦})) = π¦))} β β’ π = {β¨π, π β© β£ ((π β π΄ β§ π β (π Γ π)) β§ (π We π β§ βπ§ β π (πΉβ(β‘π β {π§})) = π§))} | ||
Theorem | fpwwelem 10515* | Lemma for fpwwe 10516. (Contributed by Mario Carneiro, 15-May-2015.) (Revised by AV, 20-Jul-2024.) |
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ (πΉβ(β‘π β {π¦})) = π¦))} & β’ (π β π΄ β π) β β’ (π β (πππ β ((π β π΄ β§ π β (π Γ π)) β§ (π We π β§ βπ¦ β π (πΉβ(β‘π β {π¦})) = π¦)))) | ||
Theorem | fpwwe 10516* | Given any function πΉ from the powerset of π΄ to π΄, canth2 9008 gives that the function is not injective, but we can say rather more than that. There is a unique well-ordered subset β¨π, (πβπ)β© which "agrees" with πΉ in the sense that each initial segment maps to its upper bound, and such that the entire set maps to an element of the set (so that it cannot be extended without losing the well-ordering). This theorem can be used to prove dfac8a 9900. Theorem 1.1 of [KanamoriPincus] p. 415. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by AV, 20-Jul-2024.) |
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ (πΉβ(β‘π β {π¦})) = π¦))} & β’ (π β π΄ β π) & β’ ((π β§ π₯ β (π« π΄ β© dom card)) β (πΉβπ₯) β π΄) & β’ π = βͺ dom π β β’ (π β ((πππ β§ (πΉβπ) β π) β (π = π β§ π = (πβπ)))) | ||
Theorem | canth4 10517* | An "effective" form of Cantor's theorem canth 7303. For any function πΉ from the powerset of π΄ to π΄, there are two definable sets π΅ and πΆ which witness non-injectivity of πΉ. Corollary 1.3 of [KanamoriPincus] p. 416. (Contributed by Mario Carneiro, 18-May-2015.) |
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ (πΉβ(β‘π β {π¦})) = π¦))} & β’ π΅ = βͺ dom π & β’ πΆ = (β‘(πβπ΅) β {(πΉβπ΅)}) β β’ ((π΄ β π β§ πΉ:π·βΆπ΄ β§ (π« π΄ β© dom card) β π·) β (π΅ β π΄ β§ πΆ β π΅ β§ (πΉβπ΅) = (πΉβπΆ))) | ||
Theorem | canthnumlem 10518* | Lemma for canthnum 10519. (Contributed by Mario Carneiro, 19-May-2015.) |
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ (πΉβ(β‘π β {π¦})) = π¦))} & β’ π΅ = βͺ dom π & β’ πΆ = (β‘(πβπ΅) β {(πΉβπ΅)}) β β’ (π΄ β π β Β¬ πΉ:(π« π΄ β© dom card)β1-1βπ΄) | ||
Theorem | canthnum 10519 | The set of well-orderable subsets of a set π΄ strictly dominates π΄. A stronger form of canth2 9008. Corollary 1.4(a) of [KanamoriPincus] p. 417. (Contributed by Mario Carneiro, 19-May-2015.) |
β’ (π΄ β π β π΄ βΊ (π« π΄ β© dom card)) | ||
Theorem | canthwelem 10520* | Lemma for canthwe 10521. (Contributed by Mario Carneiro, 31-May-2015.) |
β’ π = {β¨π₯, πβ© β£ (π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯)} & β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ [(β‘π β {π¦}) / π’](π’πΉ(π β© (π’ Γ π’))) = π¦))} & β’ π΅ = βͺ dom π & β’ πΆ = (β‘(πβπ΅) β {(π΅πΉ(πβπ΅))}) β β’ (π΄ β π β Β¬ πΉ:πβ1-1βπ΄) | ||
Theorem | canthwe 10521* | The set of well-orders of a set π΄ strictly dominates π΄. A stronger form of canth2 9008. Corollary 1.4(b) of [KanamoriPincus] p. 417. (Contributed by Mario Carneiro, 31-May-2015.) |
β’ π = {β¨π₯, πβ© β£ (π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯)} β β’ (π΄ β π β π΄ βΊ π) | ||
Theorem | canthp1lem1 10522 | Lemma for canthp1 10524. (Contributed by Mario Carneiro, 18-May-2015.) |
β’ (1o βΊ π΄ β (π΄ β 2o) βΌ π« π΄) | ||
Theorem | canthp1lem2 10523* | Lemma for canthp1 10524. (Contributed by Mario Carneiro, 18-May-2015.) |
β’ (π β 1o βΊ π΄) & β’ (π β πΉ:π« π΄β1-1-ontoβ(π΄ β 1o)) & β’ (π β πΊ:((π΄ β 1o) β {(πΉβπ΄)})β1-1-ontoβπ΄) & β’ π» = ((πΊ β πΉ) β (π₯ β π« π΄ β¦ if(π₯ = π΄, β , π₯))) & β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ (π»β(β‘π β {π¦})) = π¦))} & β’ π΅ = βͺ dom π β β’ Β¬ π | ||
Theorem | canthp1 10524 | A slightly stronger form of Cantor's theorem: For 1 < π, π + 1 < 2βπ. Corollary 1.6 of [KanamoriPincus] p. 417. (Contributed by Mario Carneiro, 18-May-2015.) |
β’ (1o βΊ π΄ β (π΄ β 1o) βΊ π« π΄) | ||
Theorem | finngch 10525 | The exclusion of finite sets from consideration in df-gch 10491 is necessary, because otherwise finite sets larger than a singleton would violate the GCH property. (Contributed by Mario Carneiro, 10-Jun-2015.) |
β’ ((π΄ β Fin β§ 1o βΊ π΄) β (π΄ βΊ (π΄ β 1o) β§ (π΄ β 1o) βΊ π« π΄)) | ||
Theorem | gchdju1 10526 | An infinite GCH-set is idempotent under cardinal successor. (Contributed by Mario Carneiro, 18-May-2015.) |
β’ ((π΄ β GCH β§ Β¬ π΄ β Fin) β (π΄ β 1o) β π΄) | ||
Theorem | gchinf 10527 | An infinite GCH-set is Dedekind-infinite. (Contributed by Mario Carneiro, 31-May-2015.) |
β’ ((π΄ β GCH β§ Β¬ π΄ β Fin) β Ο βΌ π΄) | ||
Theorem | pwfseqlem1 10528* | Lemma for pwfseq 10534. Derive a contradiction by diagonalization. (Contributed by Mario Carneiro, 31-May-2015.) |
β’ (π β πΊ:π« π΄β1-1ββͺ π β Ο (π΄ βm π)) & β’ (π β π β π΄) & β’ (π β π»:Οβ1-1-ontoβπ) & β’ (π β ((π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯) β§ Ο βΌ π₯)) & β’ ((π β§ π) β πΎ:βͺ π β Ο (π₯ βm π)β1-1βπ₯) & β’ π· = (πΊβ{π€ β π₯ β£ ((β‘πΎβπ€) β ran πΊ β§ Β¬ π€ β (β‘πΊβ(β‘πΎβπ€)))}) β β’ ((π β§ π) β π· β (βͺ π β Ο (π΄ βm π) β βͺ π β Ο (π₯ βm π))) | ||
Theorem | pwfseqlem2 10529* | Lemma for pwfseq 10534. (Contributed by Mario Carneiro, 18-Nov-2014.) (Revised by AV, 18-Sep-2021.) |
β’ (π β πΊ:π« π΄β1-1ββͺ π β Ο (π΄ βm π)) & β’ (π β π β π΄) & β’ (π β π»:Οβ1-1-ontoβπ) & β’ (π β ((π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯) β§ Ο βΌ π₯)) & β’ ((π β§ π) β πΎ:βͺ π β Ο (π₯ βm π)β1-1βπ₯) & β’ π· = (πΊβ{π€ β π₯ β£ ((β‘πΎβπ€) β ran πΊ β§ Β¬ π€ β (β‘πΊβ(β‘πΎβπ€)))}) & β’ πΉ = (π₯ β V, π β V β¦ if(π₯ β Fin, (π»β(cardβπ₯)), (π·ββ© {π§ β Ο β£ Β¬ (π·βπ§) β π₯}))) β β’ ((π β Fin β§ π β π) β (ππΉπ ) = (π»β(cardβπ))) | ||
Theorem | pwfseqlem3 10530* | Lemma for pwfseq 10534. Using the construction π· from pwfseqlem1 10528, produce a function πΉ that maps any well-ordered infinite set to an element outside the set. (Contributed by Mario Carneiro, 31-May-2015.) |
β’ (π β πΊ:π« π΄β1-1ββͺ π β Ο (π΄ βm π)) & β’ (π β π β π΄) & β’ (π β π»:Οβ1-1-ontoβπ) & β’ (π β ((π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯) β§ Ο βΌ π₯)) & β’ ((π β§ π) β πΎ:βͺ π β Ο (π₯ βm π)β1-1βπ₯) & β’ π· = (πΊβ{π€ β π₯ β£ ((β‘πΎβπ€) β ran πΊ β§ Β¬ π€ β (β‘πΊβ(β‘πΎβπ€)))}) & β’ πΉ = (π₯ β V, π β V β¦ if(π₯ β Fin, (π»β(cardβπ₯)), (π·ββ© {π§ β Ο β£ Β¬ (π·βπ§) β π₯}))) β β’ ((π β§ π) β (π₯πΉπ) β (π΄ β π₯)) | ||
Theorem | pwfseqlem4a 10531* | Lemma for pwfseqlem4 10532. (Contributed by Mario Carneiro, 7-Jun-2016.) |
β’ (π β πΊ:π« π΄β1-1ββͺ π β Ο (π΄ βm π)) & β’ (π β π β π΄) & β’ (π β π»:Οβ1-1-ontoβπ) & β’ (π β ((π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯) β§ Ο βΌ π₯)) & β’ ((π β§ π) β πΎ:βͺ π β Ο (π₯ βm π)β1-1βπ₯) & β’ π· = (πΊβ{π€ β π₯ β£ ((β‘πΎβπ€) β ran πΊ β§ Β¬ π€ β (β‘πΊβ(β‘πΎβπ€)))}) & β’ πΉ = (π₯ β V, π β V β¦ if(π₯ β Fin, (π»β(cardβπ₯)), (π·ββ© {π§ β Ο β£ Β¬ (π·βπ§) β π₯}))) β β’ ((π β§ (π β π΄ β§ π β (π Γ π) β§ π We π)) β (ππΉπ ) β π΄) | ||
Theorem | pwfseqlem4 10532* | Lemma for pwfseq 10534. Derive a final contradiction from the function πΉ in pwfseqlem3 10530. Applying fpwwe2 10513 to it, we get a certain maximal well-ordered subset π, but the defining property (ππΉ(πβπ)) β π contradicts our assumption on πΉ, so we are reduced to the case of π finite. This too is a contradiction, though, because π and its preimage under (πβπ) are distinct sets of the same cardinality and in a subset relation, which is impossible for finite sets. (Contributed by Mario Carneiro, 31-May-2015.) |
β’ (π β πΊ:π« π΄β1-1ββͺ π β Ο (π΄ βm π)) & β’ (π β π β π΄) & β’ (π β π»:Οβ1-1-ontoβπ) & β’ (π β ((π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯) β§ Ο βΌ π₯)) & β’ ((π β§ π) β πΎ:βͺ π β Ο (π₯ βm π)β1-1βπ₯) & β’ π· = (πΊβ{π€ β π₯ β£ ((β‘πΎβπ€) β ran πΊ β§ Β¬ π€ β (β‘πΊβ(β‘πΎβπ€)))}) & β’ πΉ = (π₯ β V, π β V β¦ if(π₯ β Fin, (π»β(cardβπ₯)), (π·ββ© {π§ β Ο β£ Β¬ (π·βπ§) β π₯}))) & β’ π = {β¨π, π β© β£ ((π β π΄ β§ π β (π Γ π)) β§ (π We π β§ βπ β π [(β‘π β {π}) / π£](π£πΉ(π β© (π£ Γ π£))) = π))} & β’ π = βͺ dom π β β’ Β¬ π | ||
Theorem | pwfseqlem5 10533* |
Lemma for pwfseq 10534. Although in some ways pwfseqlem4 10532 is the "main"
part of the proof, one last aspect which makes up a remark in the
original text is by far the hardest part to formalize. The main proof
relies on the existence of an injection πΎ from the set of finite
sequences on an infinite set π₯ to π₯. Now this alone would
not
be difficult to prove; this is mostly the claim of fseqen 9897. However,
what is needed for the proof is a canonical injection on these
sets,
so we have to start from scratch pulling together explicit bijections
from the lemmas.
If one attempts such a program, it will mostly go through, but there is one key step which is inherently nonconstructive, namely the proof of infxpen 9884. The resolution is not obvious, but it turns out that reversing an infinite ordinal's Cantor normal form absorbs all the non-leading terms (cnfcom3c 9576), which can be used to construct a pairing function explicitly using properties of the ordinal exponential (infxpenc 9888). (Contributed by Mario Carneiro, 31-May-2015.) |
β’ (π β πΊ:π« π΄β1-1ββͺ π β Ο (π΄ βm π)) & β’ (π β π β π΄) & β’ (π β π»:Οβ1-1-ontoβπ) & β’ (π β ((π‘ β π΄ β§ π β (π‘ Γ π‘) β§ π We π‘) β§ Ο βΌ π‘)) & β’ (π β βπ β (harβπ« π΄)(Ο β π β (πβπ):(π Γ π)β1-1-ontoβπ)) & β’ π = OrdIso(π, π‘) & β’ π = (π’ β dom π, π£ β dom π β¦ β¨(πβπ’), (πβπ£)β©) & β’ π = ((π β (πβdom π)) β β‘π) & β’ π = seqΟ((π β V, π β V β¦ (π₯ β (π‘ βm suc π) β¦ ((πβ(π₯ βΎ π))π(π₯βπ)))), {β¨β , (πββ )β©}) & β’ π = (π¦ β βͺ π β Ο (π‘ βm π) β¦ β¨dom π¦, ((πβdom π¦)βπ¦)β©) & β’ πΌ = (π₯ β Ο, π¦ β π‘ β¦ β¨(πβπ₯), π¦β©) & β’ πΎ = ((π β πΌ) β π) β β’ Β¬ π | ||
Theorem | pwfseq 10534* | The powerset of a Dedekind-infinite set does not inject into the set of finite sequences. The proof is due to Halbeisen and Shelah. Proposition 1.7 of [KanamoriPincus] p. 418. (Contributed by Mario Carneiro, 31-May-2015.) |
β’ (Ο βΌ π΄ β Β¬ π« π΄ βΌ βͺ π β Ο (π΄ βm π)) | ||
Theorem | pwxpndom2 10535 | The powerset of a Dedekind-infinite set does not inject into its Cartesian product with itself. (Contributed by Mario Carneiro, 31-May-2015.) (Proof shortened by AV, 18-Jul-2022.) |
β’ (Ο βΌ π΄ β Β¬ π« π΄ βΌ (π΄ β (π΄ Γ π΄))) | ||
Theorem | pwxpndom 10536 | The powerset of a Dedekind-infinite set does not inject into its Cartesian product with itself. (Contributed by Mario Carneiro, 31-May-2015.) |
β’ (Ο βΌ π΄ β Β¬ π« π΄ βΌ (π΄ Γ π΄)) | ||
Theorem | pwdjundom 10537 | The powerset of a Dedekind-infinite set does not inject into its cardinal sum with itself. (Contributed by Mario Carneiro, 31-May-2015.) |
β’ (Ο βΌ π΄ β Β¬ π« π΄ βΌ (π΄ β π΄)) | ||
Theorem | gchdjuidm 10538 | An infinite GCH-set is idempotent under cardinal sum. Part of Lemma 2.2 of [KanamoriPincus] p. 419. (Contributed by Mario Carneiro, 31-May-2015.) |
β’ ((π΄ β GCH β§ Β¬ π΄ β Fin) β (π΄ β π΄) β π΄) | ||
Theorem | gchxpidm 10539 | An infinite GCH-set is idempotent under cardinal product. Part of Lemma 2.2 of [KanamoriPincus] p. 419. (Contributed by Mario Carneiro, 31-May-2015.) |
β’ ((π΄ β GCH β§ Β¬ π΄ β Fin) β (π΄ Γ π΄) β π΄) | ||
Theorem | gchpwdom 10540 | A relationship between dominance over the powerset and strict dominance when the sets involved are infinite GCH-sets. Proposition 3.1 of [KanamoriPincus] p. 421. (Contributed by Mario Carneiro, 31-May-2015.) |
β’ ((Ο βΌ π΄ β§ π΄ β GCH β§ π΅ β GCH) β (π΄ βΊ π΅ β π« π΄ βΌ π΅)) | ||
Theorem | gchaleph 10541 | If (β΅βπ΄) is a GCH-set and its powerset is well-orderable, then the successor aleph (β΅βsuc π΄) is equinumerous to the powerset of (β΅βπ΄). (Contributed by Mario Carneiro, 15-May-2015.) |
β’ ((π΄ β On β§ (β΅βπ΄) β GCH β§ π« (β΅βπ΄) β dom card) β (β΅βsuc π΄) β π« (β΅βπ΄)) | ||
Theorem | gchaleph2 10542 | If (β΅βπ΄) and (β΅βsuc π΄) are GCH-sets, then the successor aleph (β΅βsuc π΄) is equinumerous to the powerset of (β΅βπ΄). (Contributed by Mario Carneiro, 31-May-2015.) |
β’ ((π΄ β On β§ (β΅βπ΄) β GCH β§ (β΅βsuc π΄) β GCH) β (β΅βsuc π΄) β π« (β΅βπ΄)) | ||
Theorem | hargch 10543 | If π΄ + β π« π΄, then π΄ is a GCH-set. The much simpler converse to gchhar 10549. (Contributed by Mario Carneiro, 2-Jun-2015.) |
β’ ((harβπ΄) β π« π΄ β π΄ β GCH) | ||
Theorem | alephgch 10544 | If (β΅βsuc π΄) is equinumerous to the powerset of (β΅βπ΄), then (β΅βπ΄) is a GCH-set. (Contributed by Mario Carneiro, 15-May-2015.) |
β’ ((β΅βsuc π΄) β π« (β΅βπ΄) β (β΅βπ΄) β GCH) | ||
Theorem | gch2 10545 | It is sufficient to require that all alephs are GCH-sets to ensure the full generalized continuum hypothesis. (The proof uses the Axiom of Regularity.) (Contributed by Mario Carneiro, 15-May-2015.) |
β’ (GCH = V β ran β΅ β GCH) | ||
Theorem | gch3 10546 | An equivalent formulation of the generalized continuum hypothesis. (Contributed by Mario Carneiro, 15-May-2015.) |
β’ (GCH = V β βπ₯ β On (β΅βsuc π₯) β π« (β΅βπ₯)) | ||
Theorem | gch-kn 10547* | The equivalence of two versions of the Generalized Continuum Hypothesis. The right-hand side is the standard version in the literature. The left-hand side is a version devised by Kannan Nambiar, which he calls the Axiom of Combinatorial Sets. For the notation and motivation behind this axiom, see his paper, "Derivation of Continuum Hypothesis from Axiom of Combinatorial Sets", available at http://www.e-atheneum.net/science/derivation_ch.pdf. The equivalence of the two sides provides a negative answer to Open Problem 2 in http://www.e-atheneum.net/science/open_problem_print.pdf. The key idea in the proof below is to equate both sides of alephexp2 10451 to the successor aleph using enen2 8996. (Contributed by NM, 1-Oct-2004.) |
β’ (π΄ β On β ((β΅βsuc π΄) β {π₯ β£ (π₯ β (β΅βπ΄) β§ π₯ β (β΅βπ΄))} β (β΅βsuc π΄) β (2o βm (β΅βπ΄)))) | ||
Theorem | gchaclem 10548 | Lemma for gchac 10551 (obsolete, used in SierpiΕski's proof). (Contributed by Mario Carneiro, 15-May-2015.) |
β’ (π β Ο βΌ π΄) & β’ (π β π« πΆ β GCH) & β’ (π β (π΄ βΌ πΆ β§ (π΅ βΌ π« πΆ β π« π΄ βΌ π΅))) β β’ (π β (π΄ βΌ π« πΆ β§ (π΅ βΌ π« π« πΆ β π« π΄ βΌ π΅))) | ||
Theorem | gchhar 10549 | A "local" form of gchac 10551. If π΄ and π« π΄ are GCH-sets, then the Hartogs number of π΄ is π« π΄ (so π« π΄ and a fortiori π΄ are well-orderable). The proof is due to Specker. Theorem 2.1 of [KanamoriPincus] p. 419. (Contributed by Mario Carneiro, 31-May-2015.) |
β’ ((Ο βΌ π΄ β§ π΄ β GCH β§ π« π΄ β GCH) β (harβπ΄) β π« π΄) | ||
Theorem | gchacg 10550 | A "local" form of gchac 10551. If π΄ and π« π΄ are GCH-sets, then π« π΄ is well-orderable. The proof is due to Specker. Theorem 2.1 of [KanamoriPincus] p. 419. (Contributed by Mario Carneiro, 15-May-2015.) |
β’ ((Ο βΌ π΄ β§ π΄ β GCH β§ π« π΄ β GCH) β π« π΄ β dom card) | ||
Theorem | gchac 10551 | The Generalized Continuum Hypothesis implies the Axiom of Choice. The original proof is due to SierpiΕski (1947); we use a refinement of SierpiΕski's result due to Specker. (Contributed by Mario Carneiro, 15-May-2015.) |
β’ (GCH = V β CHOICE) | ||
Here we introduce Tarski-Grothendieck (TG) set theory, named after mathematicians Alfred Tarski and Alexander Grothendieck. TG theory extends ZFC with the TG Axiom ax-groth 10693, which states that for every set π₯ there is an inaccessible cardinal π¦ such that π¦ is not in π₯. The addition of this axiom to ZFC set theory provides a framework for category theory, thus for all practical purposes giving us a complete foundation for "all of mathematics". We first introduce the concept of inaccessibles, including weakly and strongly inaccessible cardinals (df-wina 10554 and df-ina 10555 respectively ), Tarski classes (df-tsk 10619), and Grothendieck universes (df-gru 10661). We then introduce the Tarski's axiom ax-groth 10693 and prove various properties from that. | ||
Syntax | cwina 10552 | The class of weak inaccessibles. |
class Inaccw | ||
Syntax | cina 10553 | The class of strong inaccessibles. |
class Inacc | ||
Definition | df-wina 10554* | An ordinal is weakly inaccessible iff it is a regular limit cardinal. Note that our definition allows Ο as a weakly inaccessible cardinal. (Contributed by Mario Carneiro, 22-Jun-2013.) |
β’ Inaccw = {π₯ β£ (π₯ β β β§ (cfβπ₯) = π₯ β§ βπ¦ β π₯ βπ§ β π₯ π¦ βΊ π§)} | ||
Definition | df-ina 10555* | An ordinal is strongly inaccessible iff it is a regular strong limit cardinal, which is to say that it dominates the powersets of every smaller ordinal. (Contributed by Mario Carneiro, 22-Jun-2013.) |
β’ Inacc = {π₯ β£ (π₯ β β β§ (cfβπ₯) = π₯ β§ βπ¦ β π₯ π« π¦ βΊ π₯)} | ||
Theorem | elwina 10556* | Conditions of weak inaccessibility. (Contributed by Mario Carneiro, 22-Jun-2013.) |
β’ (π΄ β Inaccw β (π΄ β β β§ (cfβπ΄) = π΄ β§ βπ₯ β π΄ βπ¦ β π΄ π₯ βΊ π¦)) | ||
Theorem | elina 10557* | Conditions of strong inaccessibility. (Contributed by Mario Carneiro, 22-Jun-2013.) |
β’ (π΄ β Inacc β (π΄ β β β§ (cfβπ΄) = π΄ β§ βπ₯ β π΄ π« π₯ βΊ π΄)) | ||
Theorem | winaon 10558 | A weakly inaccessible cardinal is an ordinal. (Contributed by Mario Carneiro, 29-May-2014.) |
β’ (π΄ β Inaccw β π΄ β On) | ||
Theorem | inawinalem 10559* | Lemma for inawina 10560. (Contributed by Mario Carneiro, 8-Jun-2014.) |
β’ (π΄ β On β (βπ₯ β π΄ π« π₯ βΊ π΄ β βπ₯ β π΄ βπ¦ β π΄ π₯ βΊ π¦)) | ||
Theorem | inawina 10560 | Every strongly inaccessible cardinal is weakly inaccessible. (Contributed by Mario Carneiro, 29-May-2014.) |
β’ (π΄ β Inacc β π΄ β Inaccw) | ||
Theorem | omina 10561 | Ο is a strongly inaccessible cardinal. (Many definitions of "inaccessible" explicitly disallow Ο as an inaccessible cardinal, but this choice allows to reuse our results for inaccessibles for Ο.) (Contributed by Mario Carneiro, 29-May-2014.) |
β’ Ο β Inacc | ||
Theorem | winacard 10562 | A weakly inaccessible cardinal is a cardinal. (Contributed by Mario Carneiro, 29-May-2014.) |
β’ (π΄ β Inaccw β (cardβπ΄) = π΄) | ||
Theorem | winainflem 10563* | A weakly inaccessible cardinal is infinite. (Contributed by Mario Carneiro, 29-May-2014.) |
β’ ((π΄ β β β§ π΄ β On β§ βπ₯ β π΄ βπ¦ β π΄ π₯ βΊ π¦) β Ο β π΄) | ||
Theorem | winainf 10564 | A weakly inaccessible cardinal is infinite. (Contributed by Mario Carneiro, 29-May-2014.) |
β’ (π΄ β Inaccw β Ο β π΄) | ||
Theorem | winalim 10565 | A weakly inaccessible cardinal is a limit ordinal. (Contributed by Mario Carneiro, 29-May-2014.) |
β’ (π΄ β Inaccw β Lim π΄) | ||
Theorem | winalim2 10566* | A nontrivial weakly inaccessible cardinal is a limit aleph. (Contributed by Mario Carneiro, 29-May-2014.) |
β’ ((π΄ β Inaccw β§ π΄ β Ο) β βπ₯((β΅βπ₯) = π΄ β§ Lim π₯)) | ||
Theorem | winafp 10567 | A nontrivial weakly inaccessible cardinal is a fixed point of the aleph function. (Contributed by Mario Carneiro, 29-May-2014.) |
β’ ((π΄ β Inaccw β§ π΄ β Ο) β (β΅βπ΄) = π΄) | ||
Theorem | winafpi 10568 | This theorem, which states that a nontrivial inaccessible cardinal is its own aleph number, is stated here in inference form, where the assumptions are in the hypotheses rather than an antecedent. Often, we use dedth 4543 to turn this type of statement into the closed form statement winafp 10567, but in this case, since it is consistent with ZFC that there are no nontrivial inaccessible cardinals, it is not possible to prove winafp 10567 using this theorem and dedth 4543, in ZFC. (You can prove this if you use ax-groth 10693, though.) (Contributed by Mario Carneiro, 28-May-2014.) |
β’ π΄ β Inaccw & β’ π΄ β Ο β β’ (β΅βπ΄) = π΄ | ||
Theorem | gchina 10569 | Assuming the GCH, weakly and strongly inaccessible cardinals coincide. Theorem 11.20 of [TakeutiZaring] p. 106. (Contributed by Mario Carneiro, 5-Jun-2015.) |
β’ (GCH = V β Inaccw = Inacc) | ||
Syntax | cwun 10570 | Extend class definition to include the class of all weak universes. |
class WUni | ||
Syntax | cwunm 10571 | Extend class definition to include the map whose value is the smallest weak universe of which the given set is a subset. |
class wUniCl | ||
Definition | df-wun 10572* | The class of all weak universes. A weak universe is a nonempty transitive class closed under union, pairing, and powerset. The advantage of weak universes over Grothendieck universes is that one can prove that every set is contained in a weak universe in ZF (see uniwun 10610) whereas the analogue for Grothendieck universes requires ax-groth 10693 (see grothtsk 10705). (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ WUni = {π’ β£ (Tr π’ β§ π’ β β β§ βπ₯ β π’ (βͺ π₯ β π’ β§ π« π₯ β π’ β§ βπ¦ β π’ {π₯, π¦} β π’))} | ||
Definition | df-wunc 10573* | A function that maps a set π₯ to the smallest weak universe that contains the elements of the set. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ wUniCl = (π₯ β V β¦ β© {π’ β WUni β£ π₯ β π’}) | ||
Theorem | iswun 10574* | Properties of a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β (π β WUni β (Tr π β§ π β β β§ βπ₯ β π (βͺ π₯ β π β§ π« π₯ β π β§ βπ¦ β π {π₯, π¦} β π)))) | ||
Theorem | wuntr 10575 | A weak universe is transitive. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β WUni β Tr π) | ||
Theorem | wununi 10576 | A weak universe is closed under union. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β βͺ π΄ β π) | ||
Theorem | wunpw 10577 | A weak universe is closed under powerset. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β π« π΄ β π) | ||
Theorem | wunelss 10578 | The elements of a weak universe are also subsets of it. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β π΄ β π) | ||
Theorem | wunpr 10579 | A weak universe is closed under pairing. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β {π΄, π΅} β π) | ||
Theorem | wunun 10580 | A weak universe is closed under binary union. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄ βͺ π΅) β π) | ||
Theorem | wuntp 10581 | A weak universe is closed under unordered triple. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) β β’ (π β {π΄, π΅, πΆ} β π) | ||
Theorem | wunss 10582 | A weak universe is closed under subsets. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π΄) β β’ (π β π΅ β π) | ||
Theorem | wunin 10583 | A weak universe is closed under binary intersections. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β (π΄ β© π΅) β π) | ||
Theorem | wundif 10584 | A weak universe is closed under class difference. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β (π΄ β π΅) β π) | ||
Theorem | wunint 10585 | A weak universe is closed under nonempty intersections. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ ((π β§ π΄ β β ) β β© π΄ β π) | ||
Theorem | wunsn 10586 | A weak universe is closed under singletons. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β {π΄} β π) | ||
Theorem | wunsuc 10587 | A weak universe is closed under successors. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β suc π΄ β π) | ||
Theorem | wun0 10588 | A weak universe contains the empty set. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) β β’ (π β β β π) | ||
Theorem | wunr1om 10589 | A weak universe is infinite, because it contains all the finite levels of the cumulative hierarchy. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) β β’ (π β (π 1 β Ο) β π) | ||
Theorem | wunom 10590 | A weak universe contains all the finite ordinals, and hence is infinite. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) β β’ (π β Ο β π) | ||
Theorem | wunfi 10591 | A weak universe contains all finite sets with elements drawn from the universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΄ β Fin) β β’ (π β π΄ β π) | ||
Theorem | wunop 10592 | A weak universe is closed under ordered pairs. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β β¨π΄, π΅β© β π) | ||
Theorem | wunot 10593 | A weak universe is closed under ordered triples. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) β β’ (π β β¨π΄, π΅, πΆβ© β π) | ||
Theorem | wunxp 10594 | A weak universe is closed under cartesian products. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄ Γ π΅) β π) | ||
Theorem | wunpm 10595 | A weak universe is closed under partial mappings. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄ βpm π΅) β π) | ||
Theorem | wunmap 10596 | A weak universe is closed under mappings. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄ βm π΅) β π) | ||
Theorem | wunf 10597 | A weak universe is closed under functions with known domain and codomain. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΉ:π΄βΆπ΅) β β’ (π β πΉ β π) | ||
Theorem | wundm 10598 | A weak universe is closed under the domain operator. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β dom π΄ β π) | ||
Theorem | wunrn 10599 | A weak universe is closed under the range operator. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β ran π΄ β π) | ||
Theorem | wuncnv 10600 | A weak universe is closed under the converse operator. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β β‘π΄ β π) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |