Metamath Proof Explorer

Theorem inatsk

Description: ( R1A ) for A a strongly inaccessible cardinal is a Tarski class. (Contributed by Mario Carneiro, 8-Jun-2013)

Ref Expression
Assertion inatsk 
|- ( A e. Inacc -> ( R1 ` A ) e. Tarski )

Proof

Step Hyp Ref Expression
1 inawina 
 |-  ( A e. Inacc -> A e. InaccW )
2 winaon 
 |-  ( A e. InaccW -> A e. On )
3 winalim 
 |-  ( A e. InaccW -> Lim A )
4 r1lim 
 |-  ( ( A e. On /\ Lim A ) -> ( R1 ` A ) = U_ y e. A ( R1 ` y ) )
5 2 3 4 syl2anc 
 |-  ( A e. InaccW -> ( R1 ` A ) = U_ y e. A ( R1 ` y ) )
6 5 eleq2d 
 |-  ( A e. InaccW -> ( x e. ( R1 ` A ) <-> x e. U_ y e. A ( R1 ` y ) ) )
7 eliun 
 |-  ( x e. U_ y e. A ( R1 ` y ) <-> E. y e. A x e. ( R1 ` y ) )
8 6 7 bitrdi 
 |-  ( A e. InaccW -> ( x e. ( R1 ` A ) <-> E. y e. A x e. ( R1 ` y ) ) )
9 onelon 
 |-  ( ( A e. On /\ y e. A ) -> y e. On )
10 2 9 sylan 
 |-  ( ( A e. InaccW /\ y e. A ) -> y e. On )
11 r1pw 
 |-  ( y e. On -> ( x e. ( R1 ` y ) <-> ~P x e. ( R1 ` suc y ) ) )
12 10 11 syl 
 |-  ( ( A e. InaccW /\ y e. A ) -> ( x e. ( R1 ` y ) <-> ~P x e. ( R1 ` suc y ) ) )
13 limsuc 
 |-  ( Lim A -> ( y e. A <-> suc y e. A ) )
14 3 13 syl 
 |-  ( A e. InaccW -> ( y e. A <-> suc y e. A ) )
15 r1ord2 
 |-  ( A e. On -> ( suc y e. A -> ( R1 ` suc y ) C_ ( R1 ` A ) ) )
16 2 15 syl 
 |-  ( A e. InaccW -> ( suc y e. A -> ( R1 ` suc y ) C_ ( R1 ` A ) ) )
17 14 16 sylbid 
 |-  ( A e. InaccW -> ( y e. A -> ( R1 ` suc y ) C_ ( R1 ` A ) ) )
18 17 imp 
 |-  ( ( A e. InaccW /\ y e. A ) -> ( R1 ` suc y ) C_ ( R1 ` A ) )
19 18 sseld 
 |-  ( ( A e. InaccW /\ y e. A ) -> ( ~P x e. ( R1 ` suc y ) -> ~P x e. ( R1 ` A ) ) )
20 12 19 sylbid 
 |-  ( ( A e. InaccW /\ y e. A ) -> ( x e. ( R1 ` y ) -> ~P x e. ( R1 ` A ) ) )
21 20 rexlimdva 
 |-  ( A e. InaccW -> ( E. y e. A x e. ( R1 ` y ) -> ~P x e. ( R1 ` A ) ) )
22 8 21 sylbid 
 |-  ( A e. InaccW -> ( x e. ( R1 ` A ) -> ~P x e. ( R1 ` A ) ) )
23 1 22 syl 
 |-  ( A e. Inacc -> ( x e. ( R1 ` A ) -> ~P x e. ( R1 ` A ) ) )
24 23 imp 
 |-  ( ( A e. Inacc /\ x e. ( R1 ` A ) ) -> ~P x e. ( R1 ` A ) )
25 elssuni 
 |-  ( ~P x e. ( R1 ` A ) -> ~P x C_ U. ( R1 ` A ) )
26 r1tr2 
 |-  U. ( R1 ` A ) C_ ( R1 ` A )
27 25 26 sstrdi 
 |-  ( ~P x e. ( R1 ` A ) -> ~P x C_ ( R1 ` A ) )
28 24 27 jccil 
 |-  ( ( A e. Inacc /\ x e. ( R1 ` A ) ) -> ( ~P x C_ ( R1 ` A ) /\ ~P x e. ( R1 ` A ) ) )
29 28 ralrimiva 
 |-  ( A e. Inacc -> A. x e. ( R1 ` A ) ( ~P x C_ ( R1 ` A ) /\ ~P x e. ( R1 ` A ) ) )
30 1 2 syl 
 |-  ( A e. Inacc -> A e. On )
31 r1suc 
 |-  ( A e. On -> ( R1 ` suc A ) = ~P ( R1 ` A ) )
32 31 eleq2d 
 |-  ( A e. On -> ( x e. ( R1 ` suc A ) <-> x e. ~P ( R1 ` A ) ) )
33 30 32 syl 
 |-  ( A e. Inacc -> ( x e. ( R1 ` suc A ) <-> x e. ~P ( R1 ` A ) ) )
34 rankr1ai 
 |-  ( x e. ( R1 ` suc A ) -> ( rank ` x ) e. suc A )
35 33 34 syl6bir 
 |-  ( A e. Inacc -> ( x e. ~P ( R1 ` A ) -> ( rank ` x ) e. suc A ) )
36 35 imp 
 |-  ( ( A e. Inacc /\ x e. ~P ( R1 ` A ) ) -> ( rank ` x ) e. suc A )
37 fvex 
 |-  ( rank ` x ) e. _V
38 37 elsuc 
 |-  ( ( rank ` x ) e. suc A <-> ( ( rank ` x ) e. A \/ ( rank ` x ) = A ) )
39 36 38 sylib 
 |-  ( ( A e. Inacc /\ x e. ~P ( R1 ` A ) ) -> ( ( rank ` x ) e. A \/ ( rank ` x ) = A ) )
40 39 orcomd 
 |-  ( ( A e. Inacc /\ x e. ~P ( R1 ` A ) ) -> ( ( rank ` x ) = A \/ ( rank ` x ) e. A ) )
41 fvex 
 |-  ( R1 ` A ) e. _V
42 elpwi 
 |-  ( x e. ~P ( R1 ` A ) -> x C_ ( R1 ` A ) )
43 42 ad2antlr 
 |-  ( ( ( A e. Inacc /\ x e. ~P ( R1 ` A ) ) /\ ( rank ` x ) = A ) -> x C_ ( R1 ` A ) )
44 ssdomg 
 |-  ( ( R1 ` A ) e. _V -> ( x C_ ( R1 ` A ) -> x ~<_ ( R1 ` A ) ) )
45 41 43 44 mpsyl 
 |-  ( ( ( A e. Inacc /\ x e. ~P ( R1 ` A ) ) /\ ( rank ` x ) = A ) -> x ~<_ ( R1 ` A ) )
46 rankcf 
 |-  -. x ~< ( cf ` ( rank ` x ) )
47 fveq2 
 |-  ( ( rank ` x ) = A -> ( cf ` ( rank ` x ) ) = ( cf ` A ) )
48 elina 
 |-  ( A e. Inacc <-> ( A =/= (/) /\ ( cf ` A ) = A /\ A. x e. A ~P x ~< A ) )
49 48 simp2bi 
 |-  ( A e. Inacc -> ( cf ` A ) = A )
50 47 49 sylan9eqr 
 |-  ( ( A e. Inacc /\ ( rank ` x ) = A ) -> ( cf ` ( rank ` x ) ) = A )
51 50 breq2d 
 |-  ( ( A e. Inacc /\ ( rank ` x ) = A ) -> ( x ~< ( cf ` ( rank ` x ) ) <-> x ~< A ) )
52 46 51 mtbii 
 |-  ( ( A e. Inacc /\ ( rank ` x ) = A ) -> -. x ~< A )
53 inar1 
 |-  ( A e. Inacc -> ( R1 ` A ) ~~ A )
54 sdomentr 
 |-  ( ( x ~< ( R1 ` A ) /\ ( R1 ` A ) ~~ A ) -> x ~< A )
55 54 expcom 
 |-  ( ( R1 ` A ) ~~ A -> ( x ~< ( R1 ` A ) -> x ~< A ) )
56 53 55 syl 
 |-  ( A e. Inacc -> ( x ~< ( R1 ` A ) -> x ~< A ) )
57 56 adantr 
 |-  ( ( A e. Inacc /\ ( rank ` x ) = A ) -> ( x ~< ( R1 ` A ) -> x ~< A ) )
58 52 57 mtod 
 |-  ( ( A e. Inacc /\ ( rank ` x ) = A ) -> -. x ~< ( R1 ` A ) )
59 58 adantlr 
 |-  ( ( ( A e. Inacc /\ x e. ~P ( R1 ` A ) ) /\ ( rank ` x ) = A ) -> -. x ~< ( R1 ` A ) )
60 bren2 
 |-  ( x ~~ ( R1 ` A ) <-> ( x ~<_ ( R1 ` A ) /\ -. x ~< ( R1 ` A ) ) )
61 45 59 60 sylanbrc 
 |-  ( ( ( A e. Inacc /\ x e. ~P ( R1 ` A ) ) /\ ( rank ` x ) = A ) -> x ~~ ( R1 ` A ) )
62 61 ex 
 |-  ( ( A e. Inacc /\ x e. ~P ( R1 ` A ) ) -> ( ( rank ` x ) = A -> x ~~ ( R1 ` A ) ) )
63 r1elwf 
 |-  ( x e. ( R1 ` suc A ) -> x e. U. ( R1 " On ) )
64 33 63 syl6bir 
 |-  ( A e. Inacc -> ( x e. ~P ( R1 ` A ) -> x e. U. ( R1 " On ) ) )
65 64 imp 
 |-  ( ( A e. Inacc /\ x e. ~P ( R1 ` A ) ) -> x e. U. ( R1 " On ) )
66 r1fnon 
 |-  R1 Fn On
67 66 fndmi 
 |-  dom R1 = On
68 30 67 eleqtrrdi 
 |-  ( A e. Inacc -> A e. dom R1 )
69 68 adantr 
 |-  ( ( A e. Inacc /\ x e. ~P ( R1 ` A ) ) -> A e. dom R1 )
70 rankr1ag 
 |-  ( ( x e. U. ( R1 " On ) /\ A e. dom R1 ) -> ( x e. ( R1 ` A ) <-> ( rank ` x ) e. A ) )
71 65 69 70 syl2anc 
 |-  ( ( A e. Inacc /\ x e. ~P ( R1 ` A ) ) -> ( x e. ( R1 ` A ) <-> ( rank ` x ) e. A ) )
72 71 biimprd 
 |-  ( ( A e. Inacc /\ x e. ~P ( R1 ` A ) ) -> ( ( rank ` x ) e. A -> x e. ( R1 ` A ) ) )
73 62 72 orim12d 
 |-  ( ( A e. Inacc /\ x e. ~P ( R1 ` A ) ) -> ( ( ( rank ` x ) = A \/ ( rank ` x ) e. A ) -> ( x ~~ ( R1 ` A ) \/ x e. ( R1 ` A ) ) ) )
74 40 73 mpd 
 |-  ( ( A e. Inacc /\ x e. ~P ( R1 ` A ) ) -> ( x ~~ ( R1 ` A ) \/ x e. ( R1 ` A ) ) )
75 74 ralrimiva 
 |-  ( A e. Inacc -> A. x e. ~P ( R1 ` A ) ( x ~~ ( R1 ` A ) \/ x e. ( R1 ` A ) ) )
76 eltsk2g 
 |-  ( ( R1 ` A ) e. _V -> ( ( R1 ` A ) e. Tarski <-> ( A. x e. ( R1 ` A ) ( ~P x C_ ( R1 ` A ) /\ ~P x e. ( R1 ` A ) ) /\ A. x e. ~P ( R1 ` A ) ( x ~~ ( R1 ` A ) \/ x e. ( R1 ` A ) ) ) ) )
77 41 76 ax-mp 
 |-  ( ( R1 ` A ) e. Tarski <-> ( A. x e. ( R1 ` A ) ( ~P x C_ ( R1 ` A ) /\ ~P x e. ( R1 ` A ) ) /\ A. x e. ~P ( R1 ` A ) ( x ~~ ( R1 ` A ) \/ x e. ( R1 ` A ) ) ) )
78 29 75 77 sylanbrc 
 |-  ( A e. Inacc -> ( R1 ` A ) e. Tarski )