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 ⊆ ℵ ⁡ x cf ⁡ ℵ ⁡ ⋂ 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 ⁡ T x ≺ y
32 9 31 ax-mp ⊢ ∀ x ∈ card ⁡ T 𝒫 x ≺ card ⁡ T → ∀ x ∈ card ⁡ T ∃ y ∈ card ⁡ T x ≺ y
33 winainflem ⊢ card ⁡ T ≠ ∅ ∧ card ⁡ T ∈ On ∧ ∀ x ∈ card ⁡ T ∃ y ∈ card ⁡ T x ≺ y → ω ⊆ card ⁡ T
34 9 33 mp3an2 ⊢ card ⁡ T ≠ ∅ ∧ ∀ x ∈ card ⁡ T ∃ y ∈ card ⁡ T x ≺ 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 ⁡ T cf ⁡ card ⁡ T = ℵ ⁡ ⋂ x ∈ On | card ⁡ T ⊆ ℵ ⁡ x cf ⁡ ℵ ⁡ ⋂ x ∈ On | card ⁡ T ⊆ ℵ ⁡ x
42 39 41 breq12d ⊢ T ∈ Tarski ∧ T ≠ ∅ → card ⁡ T ≺ card ⁡ T cf ⁡ card ⁡ T ↔ ℵ ⁡ ⋂ x ∈ On | card ⁡ T ⊆ ℵ ⁡ x ≺ ℵ ⁡ ⋂ x ∈ On | card ⁡ T ⊆ ℵ ⁡ x cf ⁡ ℵ ⁡ ⋂ x ∈ On | card ⁡ T ⊆ ℵ ⁡ x
43 5 42 mpbiri ⊢ T ∈ Tarski ∧ T ≠ ∅ → card ⁡ T ≺ card ⁡ T cf ⁡ card ⁡ T
44 simp1 ⊢ T ∈ Tarski ∧ cf ⁡ card ⁡ T ∈ card ⁡ T ∧ x ∈ card ⁡ T cf ⁡ card ⁡ T → T ∈ Tarski
45 simp3 ⊢ T ∈ Tarski ∧ cf ⁡ card ⁡ T ∈ card ⁡ T ∧ x ∈ card ⁡ T cf ⁡ card ⁡ T → x ∈ card ⁡ T cf ⁡ card ⁡ T
46 fvex ⊢ card ⁡ T ∈ V
47 fvex ⊢ cf ⁡ card ⁡ T ∈ V
48 46 47 elmap ⊢ x ∈ card ⁡ T cf ⁡ 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 ⁡ T cf ⁡ 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 ⁡ T cf ⁡ card ⁡ T → T ∈ Tarski → x ⊆ T
63 45 44 62 sylc ⊢ T ∈ Tarski ∧ cf ⁡ card ⁡ T ∈ card ⁡ T ∧ x ∈ card ⁡ T cf ⁡ card ⁡ T → x ⊆ T
64 simp2 ⊢ T ∈ Tarski ∧ cf ⁡ card ⁡ T ∈ card ⁡ T ∧ x ∈ card ⁡ T cf ⁡ card ⁡ T → cf ⁡ card ⁡ T ∈ card ⁡ T
65 ffn ⊢ x : cf ⁡ card ⁡ T ⟶ card ⁡ T → x Fn cf ⁡ card ⁡ T
66 fndmeng ⊢ x Fn cf ⁡ 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 ⁡ T cf ⁡ card ⁡ T → cf ⁡ card ⁡ T ≈ x
69 68 ensymd ⊢ x ∈ card ⁡ T cf ⁡ 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 ⁡ T cf ⁡ card ⁡ T ∧ cf ⁡ card ⁡ T ∈ card ⁡ T → x ≺ T
73 45 64 72 syl2anc ⊢ T ∈ Tarski ∧ cf ⁡ card ⁡ T ∈ card ⁡ T ∧ x ∈ card ⁡ T cf ⁡ 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 ⁡ T cf ⁡ card ⁡ T → x ∈ T
76 75 3expia ⊢ T ∈ Tarski ∧ cf ⁡ card ⁡ T ∈ card ⁡ T → x ∈ card ⁡ T cf ⁡ card ⁡ T → x ∈ T
77 76 ssrdv ⊢ T ∈ Tarski ∧ cf ⁡ card ⁡ T ∈ card ⁡ T → card ⁡ T cf ⁡ card ⁡ T ⊆ T
78 ssdomg ⊢ T ∈ Tarski → card ⁡ T cf ⁡ card ⁡ T ⊆ T → card ⁡ T cf ⁡ card ⁡ T ≼ T
79 78 imp ⊢ T ∈ Tarski ∧ card ⁡ T cf ⁡ card ⁡ T ⊆ T → card ⁡ T cf ⁡ card ⁡ T ≼ T
80 77 79 syldan ⊢ T ∈ Tarski ∧ cf ⁡ card ⁡ T ∈ card ⁡ T → card ⁡ T cf ⁡ card ⁡ T ≼ T
81 23 adantr ⊢ T ∈ Tarski ∧ cf ⁡ card ⁡ T ∈ card ⁡ T → T ≈ card ⁡ T
82 domentr ⊢ card ⁡ T cf ⁡ card ⁡ T ≼ T ∧ T ≈ card ⁡ T → card ⁡ T cf ⁡ card ⁡ T ≼ card ⁡ T
83 80 81 82 syl2anc ⊢ T ∈ Tarski ∧ cf ⁡ card ⁡ T ∈ card ⁡ T → card ⁡ T cf ⁡ card ⁡ T ≼ card ⁡ T
84 domnsym ⊢ card ⁡ T cf ⁡ card ⁡ T ≼ card ⁡ T → ¬ card ⁡ T ≺ card ⁡ T cf ⁡ card ⁡ T
85 83 84 syl ⊢ T ∈ Tarski ∧ cf ⁡ card ⁡ T ∈ card ⁡ T → ¬ card ⁡ T ≺ card ⁡ T cf ⁡ card ⁡ T
86 85 ex ⊢ T ∈ Tarski → cf ⁡ card ⁡ T ∈ card ⁡ T → ¬ card ⁡ T ≺ card ⁡ T cf ⁡ card ⁡ T
87 86 adantr ⊢ T ∈ Tarski ∧ T ≠ ∅ → cf ⁡ card ⁡ T ∈ card ⁡ T → ¬ card ⁡ T ≺ card ⁡ T cf ⁡ 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