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 AOnR1ATarskiA=AInacc

Proof

Step Hyp Ref Expression
1 df-ne A¬A=
2 simplr AOnR1ATarskiAR1ATarski
3 simpll AOnR1ATarskiAAOn
4 onwf OnR1On
5 4 sseli AOnAR1On
6 eqid rankA=rankA
7 rankr1c AR1OnrankA=rankA¬AR1rankAAR1sucrankA
8 6 7 mpbii AR1On¬AR1rankAAR1sucrankA
9 5 8 syl AOn¬AR1rankAAR1sucrankA
10 9 simpld AOn¬AR1rankA
11 r1fnon R1FnOn
12 11 fndmi domR1=On
13 12 eleq2i AdomR1AOn
14 rankonid AdomR1rankA=A
15 13 14 bitr3i AOnrankA=A
16 fveq2 rankA=AR1rankA=R1A
17 15 16 sylbi AOnR1rankA=R1A
18 10 17 neleqtrd AOn¬AR1A
19 18 adantl R1ATarskiAOn¬AR1A
20 onssr1 AdomR1AR1A
21 13 20 sylbir AOnAR1A
22 tsken R1ATarskiAR1AAR1AAR1A
23 21 22 sylan2 R1ATarskiAOnAR1AAR1A
24 23 ord R1ATarskiAOn¬AR1AAR1A
25 19 24 mt3d R1ATarskiAOnAR1A
26 2 3 25 syl2anc AOnR1ATarskiAAR1A
27 carden2b AR1AcardA=cardR1A
28 26 27 syl AOnR1ATarskiAcardA=cardR1A
29 simpl AOnR1ATarskiAOn
30 simplr AOnR1ATarskixAR1ATarski
31 21 adantr AOnR1ATarskiAR1A
32 31 sselda AOnR1ATarskixAxR1A
33 tsksdom R1ATarskixR1AxR1A
34 30 32 33 syl2anc AOnR1ATarskixAxR1A
35 simpll AOnR1ATarskixAAOn
36 25 ensymd R1ATarskiAOnR1AA
37 30 35 36 syl2anc AOnR1ATarskixAR1AA
38 sdomentr xR1AR1AAxA
39 34 37 38 syl2anc AOnR1ATarskixAxA
40 39 ralrimiva AOnR1ATarskixAxA
41 iscard cardA=AAOnxAxA
42 29 40 41 sylanbrc AOnR1ATarskicardA=A
43 42 adantr AOnR1ATarskiAcardA=A
44 28 43 eqtr3d AOnR1ATarskiAcardR1A=A
45 r10 R1=
46 on0eln0 AOnAA
47 46 biimpar AOnAA
48 r1sdom AOnAR1R1A
49 47 48 syldan AOnAR1R1A
50 45 49 eqbrtrrid AOnAR1A
51 fvex R1AV
52 51 0sdom R1AR1A
53 50 52 sylib AOnAR1A
54 53 adantlr AOnR1ATarskiAR1A
55 tskcard R1ATarskiR1AcardR1AInacc
56 2 54 55 syl2anc AOnR1ATarskiAcardR1AInacc
57 44 56 eqeltrrd AOnR1ATarskiAAInacc
58 57 ex AOnR1ATarskiAAInacc
59 1 58 biimtrrid AOnR1ATarski¬A=AInacc
60 59 orrd AOnR1ATarskiA=AInacc
61 60 ex AOnR1ATarskiA=AInacc
62 fveq2 A=R1A=R1
63 62 45 eqtrdi A=R1A=
64 0tsk Tarski
65 63 64 eqeltrdi A=R1ATarski
66 inatsk AInaccR1ATarski
67 65 66 jaoi A=AInaccR1ATarski
68 61 67 impbid1 AOnR1ATarskiA=AInacc