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 e. Tarski /\ T =/= (/) ) -> ( card ` T ) e. Inacc )

Proof

Step Hyp Ref Expression
1 cardeq0 
 |-  ( T e. Tarski -> ( ( card ` T ) = (/) <-> T = (/) ) )
2 1 necon3bid 
 |-  ( T e. Tarski -> ( ( card ` T ) =/= (/) <-> T =/= (/) ) )
3 2 biimpar 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> ( card ` T ) =/= (/) )
4 eqid 
 |-  ( z e. ( cf ` ( aleph ` |^| { x e. On | ( card ` T ) C_ ( aleph ` x ) } ) ) |-> ( har ` ( w ` z ) ) ) = ( z e. ( cf ` ( aleph ` |^| { x e. On | ( card ` T ) C_ ( aleph ` x ) } ) ) |-> ( har ` ( w ` z ) ) )
5 4 pwcfsdom 
 |-  ( aleph ` |^| { x e. On | ( card ` T ) C_ ( aleph ` x ) } ) ~< ( ( aleph ` |^| { x e. On | ( card ` T ) C_ ( aleph ` x ) } ) ^m ( cf ` ( aleph ` |^| { x e. On | ( card ` T ) C_ ( aleph ` x ) } ) ) )
6 vpwex 
 |-  ~P x e. _V
7 6 canth2 
 |-  ~P x ~< ~P ~P x
8 simpl 
 |-  ( ( T e. Tarski /\ x e. ( card ` T ) ) -> T e. Tarski )
9 cardon 
 |-  ( card ` T ) e. On
10 9 oneli 
 |-  ( x e. ( card ` T ) -> x e. On )
11 10 adantl 
 |-  ( ( T e. Tarski /\ x e. ( card ` T ) ) -> x e. On )
12 cardsdomelir 
 |-  ( x e. ( card ` T ) -> x ~< T )
13 12 adantl 
 |-  ( ( T e. Tarski /\ x e. ( card ` T ) ) -> x ~< T )
14 tskord 
 |-  ( ( T e. Tarski /\ x e. On /\ x ~< T ) -> x e. T )
15 8 11 13 14 syl3anc 
 |-  ( ( T e. Tarski /\ x e. ( card ` T ) ) -> x e. T )
16 tskpw 
 |-  ( ( T e. Tarski /\ x e. T ) -> ~P x e. T )
17 tskpwss 
 |-  ( ( T e. Tarski /\ ~P x e. T ) -> ~P ~P x C_ T )
18 16 17 syldan 
 |-  ( ( T e. Tarski /\ x e. T ) -> ~P ~P x C_ T )
19 15 18 syldan 
 |-  ( ( T e. Tarski /\ x e. ( card ` T ) ) -> ~P ~P x C_ T )
20 ssdomg 
 |-  ( T e. Tarski -> ( ~P ~P x C_ T -> ~P ~P x ~<_ T ) )
21 8 19 20 sylc 
 |-  ( ( T e. Tarski /\ x e. ( card ` T ) ) -> ~P ~P x ~<_ T )
22 cardidg 
 |-  ( T e. Tarski -> ( card ` T ) ~~ T )
23 22 ensymd 
 |-  ( T e. Tarski -> T ~~ ( card ` T ) )
24 23 adantr 
 |-  ( ( T e. Tarski /\ x e. ( card ` T ) ) -> T ~~ ( card ` T ) )
25 domentr 
 |-  ( ( ~P ~P x ~<_ T /\ T ~~ ( card ` T ) ) -> ~P ~P x ~<_ ( card ` T ) )
26 21 24 25 syl2anc 
 |-  ( ( T e. Tarski /\ x e. ( card ` T ) ) -> ~P ~P x ~<_ ( card ` T ) )
27 sdomdomtr 
 |-  ( ( ~P x ~< ~P ~P x /\ ~P ~P x ~<_ ( card ` T ) ) -> ~P x ~< ( card ` T ) )
28 7 26 27 sylancr 
 |-  ( ( T e. Tarski /\ x e. ( card ` T ) ) -> ~P x ~< ( card ` T ) )
29 28 ralrimiva 
 |-  ( T e. Tarski -> A. x e. ( card ` T ) ~P x ~< ( card ` T ) )
30 29 adantr 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> A. x e. ( card ` T ) ~P x ~< ( card ` T ) )
31 inawinalem 
 |-  ( ( card ` T ) e. On -> ( A. x e. ( card ` T ) ~P x ~< ( card ` T ) -> A. x e. ( card ` T ) E. y e. ( card ` T ) x ~< y ) )
32 9 31 ax-mp 
 |-  ( A. x e. ( card ` T ) ~P x ~< ( card ` T ) -> A. x e. ( card ` T ) E. y e. ( card ` T ) x ~< y )
33 winainflem 
 |-  ( ( ( card ` T ) =/= (/) /\ ( card ` T ) e. On /\ A. x e. ( card ` T ) E. y e. ( card ` T ) x ~< y ) -> _om C_ ( card ` T ) )
34 9 33 mp3an2 
 |-  ( ( ( card ` T ) =/= (/) /\ A. x e. ( card ` T ) E. y e. ( card ` T ) x ~< y ) -> _om C_ ( card ` T ) )
35 32 34 sylan2 
 |-  ( ( ( card ` T ) =/= (/) /\ A. x e. ( card ` T ) ~P x ~< ( card ` T ) ) -> _om C_ ( card ` T ) )
36 3 30 35 syl2anc 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> _om C_ ( card ` T ) )
37 cardidm 
 |-  ( card ` ( card ` T ) ) = ( card ` T )
38 cardaleph 
 |-  ( ( _om C_ ( card ` T ) /\ ( card ` ( card ` T ) ) = ( card ` T ) ) -> ( card ` T ) = ( aleph ` |^| { x e. On | ( card ` T ) C_ ( aleph ` x ) } ) )
39 36 37 38 sylancl 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> ( card ` T ) = ( aleph ` |^| { x e. On | ( card ` T ) C_ ( aleph ` x ) } ) )
40 39 fveq2d 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> ( cf ` ( card ` T ) ) = ( cf ` ( aleph ` |^| { x e. On | ( card ` T ) C_ ( aleph ` x ) } ) ) )
41 39 40 oveq12d 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) = ( ( aleph ` |^| { x e. On | ( card ` T ) C_ ( aleph ` x ) } ) ^m ( cf ` ( aleph ` |^| { x e. On | ( card ` T ) C_ ( aleph ` x ) } ) ) ) )
42 39 41 breq12d 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> ( ( card ` T ) ~< ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) <-> ( aleph ` |^| { x e. On | ( card ` T ) C_ ( aleph ` x ) } ) ~< ( ( aleph ` |^| { x e. On | ( card ` T ) C_ ( aleph ` x ) } ) ^m ( cf ` ( aleph ` |^| { x e. On | ( card ` T ) C_ ( aleph ` x ) } ) ) ) ) )
43 5 42 mpbiri 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> ( card ` T ) ~< ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) )
44 simp1 
 |-  ( ( T e. Tarski /\ ( cf ` ( card ` T ) ) e. ( card ` T ) /\ x e. ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) ) -> T e. Tarski )
45 simp3 
 |-  ( ( T e. Tarski /\ ( cf ` ( card ` T ) ) e. ( card ` T ) /\ x e. ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) ) -> x e. ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) )
46 fvex 
 |-  ( card ` T ) e. _V
47 fvex 
 |-  ( cf ` ( card ` T ) ) e. _V
48 46 47 elmap 
 |-  ( x e. ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) <-> x : ( cf ` ( card ` T ) ) --> ( card ` T ) )
49 fssxp 
 |-  ( x : ( cf ` ( card ` T ) ) --> ( card ` T ) -> x C_ ( ( cf ` ( card ` T ) ) X. ( card ` T ) ) )
50 48 49 sylbi 
 |-  ( x e. ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) -> x C_ ( ( cf ` ( card ` T ) ) X. ( card ` T ) ) )
51 15 ex 
 |-  ( T e. Tarski -> ( x e. ( card ` T ) -> x e. T ) )
52 51 ssrdv 
 |-  ( T e. Tarski -> ( card ` T ) C_ T )
53 cfle 
 |-  ( cf ` ( card ` T ) ) C_ ( card ` T )
54 sstr 
 |-  ( ( ( cf ` ( card ` T ) ) C_ ( card ` T ) /\ ( card ` T ) C_ T ) -> ( cf ` ( card ` T ) ) C_ T )
55 53 54 mpan 
 |-  ( ( card ` T ) C_ T -> ( cf ` ( card ` T ) ) C_ T )
56 tskxpss 
 |-  ( ( T e. Tarski /\ ( cf ` ( card ` T ) ) C_ T /\ ( card ` T ) C_ T ) -> ( ( cf ` ( card ` T ) ) X. ( card ` T ) ) C_ T )
57 56 3exp 
 |-  ( T e. Tarski -> ( ( cf ` ( card ` T ) ) C_ T -> ( ( card ` T ) C_ T -> ( ( cf ` ( card ` T ) ) X. ( card ` T ) ) C_ T ) ) )
58 57 com23 
 |-  ( T e. Tarski -> ( ( card ` T ) C_ T -> ( ( cf ` ( card ` T ) ) C_ T -> ( ( cf ` ( card ` T ) ) X. ( card ` T ) ) C_ T ) ) )
59 55 58 mpdi 
 |-  ( T e. Tarski -> ( ( card ` T ) C_ T -> ( ( cf ` ( card ` T ) ) X. ( card ` T ) ) C_ T ) )
60 52 59 mpd 
 |-  ( T e. Tarski -> ( ( cf ` ( card ` T ) ) X. ( card ` T ) ) C_ T )
61 sstr2 
 |-  ( x C_ ( ( cf ` ( card ` T ) ) X. ( card ` T ) ) -> ( ( ( cf ` ( card ` T ) ) X. ( card ` T ) ) C_ T -> x C_ T ) )
62 50 60 61 syl2im 
 |-  ( x e. ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) -> ( T e. Tarski -> x C_ T ) )
63 45 44 62 sylc 
 |-  ( ( T e. Tarski /\ ( cf ` ( card ` T ) ) e. ( card ` T ) /\ x e. ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) ) -> x C_ T )
64 simp2 
 |-  ( ( T e. Tarski /\ ( cf ` ( card ` T ) ) e. ( card ` T ) /\ x e. ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) ) -> ( cf ` ( card ` T ) ) e. ( 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 ) ) e. _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 e. ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) -> ( cf ` ( card ` T ) ) ~~ x )
69 68 ensymd 
 |-  ( x e. ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) -> x ~~ ( cf ` ( card ` T ) ) )
70 cardsdomelir 
 |-  ( ( cf ` ( card ` T ) ) e. ( card ` T ) -> ( cf ` ( card ` T ) ) ~< T )
71 ensdomtr 
 |-  ( ( x ~~ ( cf ` ( card ` T ) ) /\ ( cf ` ( card ` T ) ) ~< T ) -> x ~< T )
72 69 70 71 syl2an 
 |-  ( ( x e. ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) /\ ( cf ` ( card ` T ) ) e. ( card ` T ) ) -> x ~< T )
73 45 64 72 syl2anc 
 |-  ( ( T e. Tarski /\ ( cf ` ( card ` T ) ) e. ( card ` T ) /\ x e. ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) ) -> x ~< T )
74 tskssel 
 |-  ( ( T e. Tarski /\ x C_ T /\ x ~< T ) -> x e. T )
75 44 63 73 74 syl3anc 
 |-  ( ( T e. Tarski /\ ( cf ` ( card ` T ) ) e. ( card ` T ) /\ x e. ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) ) -> x e. T )
76 75 3expia 
 |-  ( ( T e. Tarski /\ ( cf ` ( card ` T ) ) e. ( card ` T ) ) -> ( x e. ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) -> x e. T ) )
77 76 ssrdv 
 |-  ( ( T e. Tarski /\ ( cf ` ( card ` T ) ) e. ( card ` T ) ) -> ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) C_ T )
78 ssdomg 
 |-  ( T e. Tarski -> ( ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) C_ T -> ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) ~<_ T ) )
79 78 imp 
 |-  ( ( T e. Tarski /\ ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) C_ T ) -> ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) ~<_ T )
80 77 79 syldan 
 |-  ( ( T e. Tarski /\ ( cf ` ( card ` T ) ) e. ( card ` T ) ) -> ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) ~<_ T )
81 23 adantr 
 |-  ( ( T e. Tarski /\ ( cf ` ( card ` T ) ) e. ( card ` T ) ) -> T ~~ ( card ` T ) )
82 domentr 
 |-  ( ( ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) ~<_ T /\ T ~~ ( card ` T ) ) -> ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) ~<_ ( card ` T ) )
83 80 81 82 syl2anc 
 |-  ( ( T e. Tarski /\ ( cf ` ( card ` T ) ) e. ( card ` T ) ) -> ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) ~<_ ( card ` T ) )
84 domnsym 
 |-  ( ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) ~<_ ( card ` T ) -> -. ( card ` T ) ~< ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) )
85 83 84 syl 
 |-  ( ( T e. Tarski /\ ( cf ` ( card ` T ) ) e. ( card ` T ) ) -> -. ( card ` T ) ~< ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) )
86 85 ex 
 |-  ( T e. Tarski -> ( ( cf ` ( card ` T ) ) e. ( card ` T ) -> -. ( card ` T ) ~< ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) ) )
87 86 adantr 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> ( ( cf ` ( card ` T ) ) e. ( card ` T ) -> -. ( card ` T ) ~< ( ( card ` T ) ^m ( cf ` ( card ` T ) ) ) ) )
88 43 87 mt2d 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> -. ( cf ` ( card ` T ) ) e. ( card ` T ) )
89 cfon 
 |-  ( cf ` ( card ` T ) ) e. On
90 89 9 onsseli 
 |-  ( ( cf ` ( card ` T ) ) C_ ( card ` T ) <-> ( ( cf ` ( card ` T ) ) e. ( card ` T ) \/ ( cf ` ( card ` T ) ) = ( card ` T ) ) )
91 53 90 mpbi 
 |-  ( ( cf ` ( card ` T ) ) e. ( card ` T ) \/ ( cf ` ( card ` T ) ) = ( card ` T ) )
92 91 ori 
 |-  ( -. ( cf ` ( card ` T ) ) e. ( card ` T ) -> ( cf ` ( card ` T ) ) = ( card ` T ) )
93 88 92 syl 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> ( cf ` ( card ` T ) ) = ( card ` T ) )
94 elina 
 |-  ( ( card ` T ) e. Inacc <-> ( ( card ` T ) =/= (/) /\ ( cf ` ( card ` T ) ) = ( card ` T ) /\ A. x e. ( card ` T ) ~P x ~< ( card ` T ) ) )
95 3 93 30 94 syl3anbrc 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> ( card ` T ) e. Inacc )