Metamath Proof Explorer

Theorem tskcard

Description: An even more direct relationship than r1tskina to get an inaccessible cardinal out of a Tarski class: the size of any nonempty Tarski class is an inaccessible cardinal. (Contributed by Mario Carneiro, 9-Jun-2013)

Ref Expression
Assertion tskcard ⊢T∈Tarski∧T≠∅→card⁡T∈Inacc

Proof

Step Hyp Ref Expression
1 cardeq0 ⊢T∈Tarski→card⁡T=∅↔T=∅
2 1 necon3bid ⊢T∈Tarski→card⁡T≠∅↔T≠∅
3 2 biimpar ⊢T∈Tarski∧T≠∅→card⁡T≠∅
4 eqid ⊢z∈cf⁡ℵ⁡⋂x∈On|card⁡T⊆ℵ⁡x⟼har⁡w⁡z=z∈cf⁡ℵ⁡⋂x∈On|card⁡T⊆ℵ⁡x⟼har⁡w⁡z
5 4 pwcfsdom ⊢ℵ⁡⋂x∈On|card⁡T⊆ℵ⁡x≺ℵ⁡⋂x∈On|card⁡T⊆ℵ⁡xcf⁡ℵ⁡⋂x∈On|card⁡T⊆ℵ⁡x
6 vpwex ⊢𝒫x∈V
7 6 canth2 ⊢𝒫x≺𝒫𝒫x
8 simpl ⊢T∈Tarski∧x∈card⁡T→T∈Tarski
9 cardon ⊢card⁡T∈On
10 9 oneli ⊢x∈card⁡T→x∈On
11 10 adantl ⊢T∈Tarski∧x∈card⁡T→x∈On
12 cardsdomelir ⊢x∈card⁡T→x≺T
13 12 adantl ⊢T∈Tarski∧x∈card⁡T→x≺T
14 tskord ⊢T∈Tarski∧x∈On∧x≺T→x∈T
15 8 11 13 14 syl3anc ⊢T∈Tarski∧x∈card⁡T→x∈T
16 tskpw ⊢T∈Tarski∧x∈T→𝒫x∈T
17 tskpwss ⊢T∈Tarski∧𝒫x∈T→𝒫𝒫x⊆T
18 16 17 syldan ⊢T∈Tarski∧x∈T→𝒫𝒫x⊆T
19 15 18 syldan ⊢T∈Tarski∧x∈card⁡T→𝒫𝒫x⊆T
20 ssdomg ⊢T∈Tarski→𝒫𝒫x⊆T→𝒫𝒫x≼T
21 8 19 20 sylc ⊢T∈Tarski∧x∈card⁡T→𝒫𝒫x≼T
22 cardidg ⊢T∈Tarski→card⁡T≈T
23 22 ensymd ⊢T∈Tarski→T≈card⁡T
24 23 adantr ⊢T∈Tarski∧x∈card⁡T→T≈card⁡T
25 domentr ⊢𝒫𝒫x≼T∧T≈card⁡T→𝒫𝒫x≼card⁡T
26 21 24 25 syl2anc ⊢T∈Tarski∧x∈card⁡T→𝒫𝒫x≼card⁡T
27 sdomdomtr ⊢𝒫x≺𝒫𝒫x∧𝒫𝒫x≼card⁡T→𝒫x≺card⁡T
28 7 26 27 sylancr ⊢T∈Tarski∧x∈card⁡T→𝒫x≺card⁡T
29 28 ralrimiva ⊢T∈Tarski→∀x∈card⁡T𝒫x≺card⁡T
30 29 adantr ⊢T∈Tarski∧T≠∅→∀x∈card⁡T𝒫x≺card⁡T
31 inawinalem ⊢card⁡T∈On→∀x∈card⁡T𝒫x≺card⁡T→∀x∈card⁡T∃y∈card⁡Tx≺y
32 9 31 ax-mp ⊢∀x∈card⁡T𝒫x≺card⁡T→∀x∈card⁡T∃y∈card⁡Tx≺y
33 winainflem ⊢card⁡T≠∅∧card⁡T∈On∧∀x∈card⁡T∃y∈card⁡Tx≺y→ω⊆card⁡T
34 9 33 mp3an2 ⊢card⁡T≠∅∧∀x∈card⁡T∃y∈card⁡Tx≺y→ω⊆card⁡T
35 32 34 sylan2 ⊢card⁡T≠∅∧∀x∈card⁡T𝒫x≺card⁡T→ω⊆card⁡T
36 3 30 35 syl2anc ⊢T∈Tarski∧T≠∅→ω⊆card⁡T
37 cardidm ⊢card⁡card⁡T=card⁡T
38 cardaleph ⊢ω⊆card⁡T∧card⁡card⁡T=card⁡T→card⁡T=ℵ⁡⋂x∈On|card⁡T⊆ℵ⁡x
39 36 37 38 sylancl ⊢T∈Tarski∧T≠∅→card⁡T=ℵ⁡⋂x∈On|card⁡T⊆ℵ⁡x
40 39 fveq2d ⊢T∈Tarski∧T≠∅→cf⁡card⁡T=cf⁡ℵ⁡⋂x∈On|card⁡T⊆ℵ⁡x
41 39 40 oveq12d ⊢T∈Tarski∧T≠∅→card⁡Tcf⁡card⁡T=ℵ⁡⋂x∈On|card⁡T⊆ℵ⁡xcf⁡ℵ⁡⋂x∈On|card⁡T⊆ℵ⁡x
42 39 41 breq12d ⊢T∈Tarski∧T≠∅→card⁡T≺card⁡Tcf⁡card⁡T↔ℵ⁡⋂x∈On|card⁡T⊆ℵ⁡x≺ℵ⁡⋂x∈On|card⁡T⊆ℵ⁡xcf⁡ℵ⁡⋂x∈On|card⁡T⊆ℵ⁡x
43 5 42 mpbiri ⊢T∈Tarski∧T≠∅→card⁡T≺card⁡Tcf⁡card⁡T
44 simp1 ⊢T∈Tarski∧cf⁡card⁡T∈card⁡T∧x∈card⁡Tcf⁡card⁡T→T∈Tarski
45 simp3 ⊢T∈Tarski∧cf⁡card⁡T∈card⁡T∧x∈card⁡Tcf⁡card⁡T→x∈card⁡Tcf⁡card⁡T
46 fvex ⊢card⁡T∈V
47 fvex ⊢cf⁡card⁡T∈V
48 46 47 elmap ⊢x∈card⁡Tcf⁡card⁡T↔x:cf⁡card⁡T⟶card⁡T
49 fssxp ⊢x:cf⁡card⁡T⟶card⁡T→x⊆cf⁡card⁡T×card⁡T
50 48 49 sylbi ⊢x∈card⁡Tcf⁡card⁡T→x⊆cf⁡card⁡T×card⁡T
51 15 ex ⊢T∈Tarski→x∈card⁡T→x∈T
52 51 ssrdv ⊢T∈Tarski→card⁡T⊆T
53 cfle ⊢cf⁡card⁡T⊆card⁡T
54 sstr ⊢cf⁡card⁡T⊆card⁡T∧card⁡T⊆T→cf⁡card⁡T⊆T
55 53 54 mpan ⊢card⁡T⊆T→cf⁡card⁡T⊆T
56 tskxpss ⊢T∈Tarski∧cf⁡card⁡T⊆T∧card⁡T⊆T→cf⁡card⁡T×card⁡T⊆T
57 56 3exp ⊢T∈Tarski→cf⁡card⁡T⊆T→card⁡T⊆T→cf⁡card⁡T×card⁡T⊆T
58 57 com23 ⊢T∈Tarski→card⁡T⊆T→cf⁡card⁡T⊆T→cf⁡card⁡T×card⁡T⊆T
59 55 58 mpdi ⊢T∈Tarski→card⁡T⊆T→cf⁡card⁡T×card⁡T⊆T
60 52 59 mpd ⊢T∈Tarski→cf⁡card⁡T×card⁡T⊆T
61 sstr2 ⊢x⊆cf⁡card⁡T×card⁡T→cf⁡card⁡T×card⁡T⊆T→x⊆T
62 50 60 61 syl2im ⊢x∈card⁡Tcf⁡card⁡T→T∈Tarski→x⊆T
63 45 44 62 sylc ⊢T∈Tarski∧cf⁡card⁡T∈card⁡T∧x∈card⁡Tcf⁡card⁡T→x⊆T
64 simp2 ⊢T∈Tarski∧cf⁡card⁡T∈card⁡T∧x∈card⁡Tcf⁡card⁡T→cf⁡card⁡T∈card⁡T
65 ffn ⊢x:cf⁡card⁡T⟶card⁡T→xFncf⁡card⁡T
66 fndmeng ⊢xFncf⁡card⁡T∧cf⁡card⁡T∈V→cf⁡card⁡T≈x
67 65 47 66 sylancl ⊢x:cf⁡card⁡T⟶card⁡T→cf⁡card⁡T≈x
68 48 67 sylbi ⊢x∈card⁡Tcf⁡card⁡T→cf⁡card⁡T≈x
69 68 ensymd ⊢x∈card⁡Tcf⁡card⁡T→x≈cf⁡card⁡T
70 cardsdomelir ⊢cf⁡card⁡T∈card⁡T→cf⁡card⁡T≺T
71 ensdomtr ⊢x≈cf⁡card⁡T∧cf⁡card⁡T≺T→x≺T
72 69 70 71 syl2an ⊢x∈card⁡Tcf⁡card⁡T∧cf⁡card⁡T∈card⁡T→x≺T
73 45 64 72 syl2anc ⊢T∈Tarski∧cf⁡card⁡T∈card⁡T∧x∈card⁡Tcf⁡card⁡T→x≺T
74 tskssel ⊢T∈Tarski∧x⊆T∧x≺T→x∈T
75 44 63 73 74 syl3anc ⊢T∈Tarski∧cf⁡card⁡T∈card⁡T∧x∈card⁡Tcf⁡card⁡T→x∈T
76 75 3expia ⊢T∈Tarski∧cf⁡card⁡T∈card⁡T→x∈card⁡Tcf⁡card⁡T→x∈T
77 76 ssrdv ⊢T∈Tarski∧cf⁡card⁡T∈card⁡T→card⁡Tcf⁡card⁡T⊆T
78 ssdomg ⊢T∈Tarski→card⁡Tcf⁡card⁡T⊆T→card⁡Tcf⁡card⁡T≼T
79 78 imp ⊢T∈Tarski∧card⁡Tcf⁡card⁡T⊆T→card⁡Tcf⁡card⁡T≼T
80 77 79 syldan ⊢T∈Tarski∧cf⁡card⁡T∈card⁡T→card⁡Tcf⁡card⁡T≼T
81 23 adantr ⊢T∈Tarski∧cf⁡card⁡T∈card⁡T→T≈card⁡T
82 domentr ⊢card⁡Tcf⁡card⁡T≼T∧T≈card⁡T→card⁡Tcf⁡card⁡T≼card⁡T
83 80 81 82 syl2anc ⊢T∈Tarski∧cf⁡card⁡T∈card⁡T→card⁡Tcf⁡card⁡T≼card⁡T
84 domnsym ⊢card⁡Tcf⁡card⁡T≼card⁡T→¬card⁡T≺card⁡Tcf⁡card⁡T
85 83 84 syl ⊢T∈Tarski∧cf⁡card⁡T∈card⁡T→¬card⁡T≺card⁡Tcf⁡card⁡T
86 85 ex ⊢T∈Tarski→cf⁡card⁡T∈card⁡T→¬card⁡T≺card⁡Tcf⁡card⁡T
87 86 adantr ⊢T∈Tarski∧T≠∅→cf⁡card⁡T∈card⁡T→¬card⁡T≺card⁡Tcf⁡card⁡T
88 43 87 mt2d ⊢T∈Tarski∧T≠∅→¬cf⁡card⁡T∈card⁡T
89 cfon ⊢cf⁡card⁡T∈On
90 89 9 onsseli ⊢cf⁡card⁡T⊆card⁡T↔cf⁡card⁡T∈card⁡T∨cf⁡card⁡T=card⁡T
91 53 90 mpbi ⊢cf⁡card⁡T∈card⁡T∨cf⁡card⁡T=card⁡T
92 91 ori ⊢¬cf⁡card⁡T∈card⁡T→cf⁡card⁡T=card⁡T
93 88 92 syl ⊢T∈Tarski∧T≠∅→cf⁡card⁡T=card⁡T
94 elina ⊢card⁡T∈Inacc↔card⁡T≠∅∧cf⁡card⁡T=card⁡T∧∀x∈card⁡T𝒫x≺card⁡T
95 3 93 30 94 syl3anbrc ⊢T∈Tarski∧T≠∅→card⁡T∈Inacc