Metamath Proof Explorer

Theorem r1tskina

Description: There is a direct relationship between transitive Tarski classes and inaccessible cardinals: the Tarski classes that occur in the cumulative hierarchy are exactly at the strongly inaccessible cardinals. (Contributed by Mario Carneiro, 8-Jun-2013)

Ref Expression
Assertion r1tskina 
|- ( A e. On -> ( ( R1 ` A ) e. Tarski <-> ( A = (/) \/ A e. Inacc ) ) )

Proof

Step Hyp Ref Expression
1 df-ne 
 |-  ( A =/= (/) <-> -. A = (/) )
2 simplr 
 |-  ( ( ( A e. On /\ ( R1 ` A ) e. Tarski ) /\ A =/= (/) ) -> ( R1 ` A ) e. Tarski )
3 simpll 
 |-  ( ( ( A e. On /\ ( R1 ` A ) e. Tarski ) /\ A =/= (/) ) -> A e. On )
4 onwf 
 |-  On C_ U. ( R1 " On )
5 4 sseli 
 |-  ( A e. On -> A e. U. ( R1 " On ) )
6 eqid 
 |-  ( rank ` A ) = ( rank ` A )
7 rankr1c 
 |-  ( A e. U. ( R1 " On ) -> ( ( rank ` A ) = ( rank ` A ) <-> ( -. A e. ( R1 ` ( rank ` A ) ) /\ A e. ( R1 ` suc ( rank ` A ) ) ) ) )
8 6 7 mpbii 
 |-  ( A e. U. ( R1 " On ) -> ( -. A e. ( R1 ` ( rank ` A ) ) /\ A e. ( R1 ` suc ( rank ` A ) ) ) )
9 5 8 syl 
 |-  ( A e. On -> ( -. A e. ( R1 ` ( rank ` A ) ) /\ A e. ( R1 ` suc ( rank ` A ) ) ) )
10 9 simpld 
 |-  ( A e. On -> -. A e. ( R1 ` ( rank ` A ) ) )
11 r1fnon 
 |-  R1 Fn On
12 11 fndmi 
 |-  dom R1 = On
13 12 eleq2i 
 |-  ( A e. dom R1 <-> A e. On )
14 rankonid 
 |-  ( A e. dom R1 <-> ( rank ` A ) = A )
15 13 14 bitr3i 
 |-  ( A e. On <-> ( rank ` A ) = A )
16 fveq2 
 |-  ( ( rank ` A ) = A -> ( R1 ` ( rank ` A ) ) = ( R1 ` A ) )
17 15 16 sylbi 
 |-  ( A e. On -> ( R1 ` ( rank ` A ) ) = ( R1 ` A ) )
18 10 17 neleqtrd 
 |-  ( A e. On -> -. A e. ( R1 ` A ) )
19 18 adantl 
 |-  ( ( ( R1 ` A ) e. Tarski /\ A e. On ) -> -. A e. ( R1 ` A ) )
20 onssr1 
 |-  ( A e. dom R1 -> A C_ ( R1 ` A ) )
21 13 20 sylbir 
 |-  ( A e. On -> A C_ ( R1 ` A ) )
22 tsken 
 |-  ( ( ( R1 ` A ) e. Tarski /\ A C_ ( R1 ` A ) ) -> ( A ~~ ( R1 ` A ) \/ A e. ( R1 ` A ) ) )
23 21 22 sylan2 
 |-  ( ( ( R1 ` A ) e. Tarski /\ A e. On ) -> ( A ~~ ( R1 ` A ) \/ A e. ( R1 ` A ) ) )
24 23 ord 
 |-  ( ( ( R1 ` A ) e. Tarski /\ A e. On ) -> ( -. A ~~ ( R1 ` A ) -> A e. ( R1 ` A ) ) )
25 19 24 mt3d 
 |-  ( ( ( R1 ` A ) e. Tarski /\ A e. On ) -> A ~~ ( R1 ` A ) )
26 2 3 25 syl2anc 
 |-  ( ( ( A e. On /\ ( R1 ` A ) e. Tarski ) /\ A =/= (/) ) -> A ~~ ( R1 ` A ) )
27 carden2b 
 |-  ( A ~~ ( R1 ` A ) -> ( card ` A ) = ( card ` ( R1 ` A ) ) )
28 26 27 syl 
 |-  ( ( ( A e. On /\ ( R1 ` A ) e. Tarski ) /\ A =/= (/) ) -> ( card ` A ) = ( card ` ( R1 ` A ) ) )
29 simpl 
 |-  ( ( A e. On /\ ( R1 ` A ) e. Tarski ) -> A e. On )
30 simplr 
 |-  ( ( ( A e. On /\ ( R1 ` A ) e. Tarski ) /\ x e. A ) -> ( R1 ` A ) e. Tarski )
31 21 adantr 
 |-  ( ( A e. On /\ ( R1 ` A ) e. Tarski ) -> A C_ ( R1 ` A ) )
32 31 sselda 
 |-  ( ( ( A e. On /\ ( R1 ` A ) e. Tarski ) /\ x e. A ) -> x e. ( R1 ` A ) )
33 tsksdom 
 |-  ( ( ( R1 ` A ) e. Tarski /\ x e. ( R1 ` A ) ) -> x ~< ( R1 ` A ) )
34 30 32 33 syl2anc 
 |-  ( ( ( A e. On /\ ( R1 ` A ) e. Tarski ) /\ x e. A ) -> x ~< ( R1 ` A ) )
35 simpll 
 |-  ( ( ( A e. On /\ ( R1 ` A ) e. Tarski ) /\ x e. A ) -> A e. On )
36 25 ensymd 
 |-  ( ( ( R1 ` A ) e. Tarski /\ A e. On ) -> ( R1 ` A ) ~~ A )
37 30 35 36 syl2anc 
 |-  ( ( ( A e. On /\ ( R1 ` A ) e. Tarski ) /\ x e. A ) -> ( R1 ` A ) ~~ A )
38 sdomentr 
 |-  ( ( x ~< ( R1 ` A ) /\ ( R1 ` A ) ~~ A ) -> x ~< A )
39 34 37 38 syl2anc 
 |-  ( ( ( A e. On /\ ( R1 ` A ) e. Tarski ) /\ x e. A ) -> x ~< A )
40 39 ralrimiva 
 |-  ( ( A e. On /\ ( R1 ` A ) e. Tarski ) -> A. x e. A x ~< A )
41 iscard 
 |-  ( ( card ` A ) = A <-> ( A e. On /\ A. x e. A x ~< A ) )
42 29 40 41 sylanbrc 
 |-  ( ( A e. On /\ ( R1 ` A ) e. Tarski ) -> ( card ` A ) = A )
43 42 adantr 
 |-  ( ( ( A e. On /\ ( R1 ` A ) e. Tarski ) /\ A =/= (/) ) -> ( card ` A ) = A )
44 28 43 eqtr3d 
 |-  ( ( ( A e. On /\ ( R1 ` A ) e. Tarski ) /\ A =/= (/) ) -> ( card ` ( R1 ` A ) ) = A )
45 r10 
 |-  ( R1 ` (/) ) = (/)
46 on0eln0 
 |-  ( A e. On -> ( (/) e. A <-> A =/= (/) ) )
47 46 biimpar 
 |-  ( ( A e. On /\ A =/= (/) ) -> (/) e. A )
48 r1sdom 
 |-  ( ( A e. On /\ (/) e. A ) -> ( R1 ` (/) ) ~< ( R1 ` A ) )
49 47 48 syldan 
 |-  ( ( A e. On /\ A =/= (/) ) -> ( R1 ` (/) ) ~< ( R1 ` A ) )
50 45 49 eqbrtrrid 
 |-  ( ( A e. On /\ A =/= (/) ) -> (/) ~< ( R1 ` A ) )
51 fvex 
 |-  ( R1 ` A ) e. _V
52 51 0sdom 
 |-  ( (/) ~< ( R1 ` A ) <-> ( R1 ` A ) =/= (/) )
53 50 52 sylib 
 |-  ( ( A e. On /\ A =/= (/) ) -> ( R1 ` A ) =/= (/) )
54 53 adantlr 
 |-  ( ( ( A e. On /\ ( R1 ` A ) e. Tarski ) /\ A =/= (/) ) -> ( R1 ` A ) =/= (/) )
55 tskcard 
 |-  ( ( ( R1 ` A ) e. Tarski /\ ( R1 ` A ) =/= (/) ) -> ( card ` ( R1 ` A ) ) e. Inacc )
56 2 54 55 syl2anc 
 |-  ( ( ( A e. On /\ ( R1 ` A ) e. Tarski ) /\ A =/= (/) ) -> ( card ` ( R1 ` A ) ) e. Inacc )
57 44 56 eqeltrrd 
 |-  ( ( ( A e. On /\ ( R1 ` A ) e. Tarski ) /\ A =/= (/) ) -> A e. Inacc )
58 57 ex 
 |-  ( ( A e. On /\ ( R1 ` A ) e. Tarski ) -> ( A =/= (/) -> A e. Inacc ) )
59 1 58 syl5bir 
 |-  ( ( A e. On /\ ( R1 ` A ) e. Tarski ) -> ( -. A = (/) -> A e. Inacc ) )
60 59 orrd 
 |-  ( ( A e. On /\ ( R1 ` A ) e. Tarski ) -> ( A = (/) \/ A e. Inacc ) )
61 60 ex 
 |-  ( A e. On -> ( ( R1 ` A ) e. Tarski -> ( A = (/) \/ A e. Inacc ) ) )
62 fveq2 
 |-  ( A = (/) -> ( R1 ` A ) = ( R1 ` (/) ) )
63 62 45 eqtrdi 
 |-  ( A = (/) -> ( R1 ` A ) = (/) )
64 0tsk 
 |-  (/) e. Tarski
65 63 64 eqeltrdi 
 |-  ( A = (/) -> ( R1 ` A ) e. Tarski )
66 inatsk 
 |-  ( A e. Inacc -> ( R1 ` A ) e. Tarski )
67 65 66 jaoi 
 |-  ( ( A = (/) \/ A e. Inacc ) -> ( R1 ` A ) e. Tarski )
68 61 67 impbid1 
 |-  ( A e. On -> ( ( R1 ` A ) e. Tarski <-> ( A = (/) \/ A e. Inacc ) ) )