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