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 ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ( card ‘ 𝑇 ) ∈ Inacc )

Proof

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