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 ( 𝐴 ∈ On → ( ( 𝑅1 ‘ 𝐴 ) ∈ Tarski ↔ ( 𝐴 = ∅ ∨ 𝐴 ∈ Inacc ) ) )

Proof

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