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 ( 𝐴 ∈ Inacc → ( 𝑅1 ‘ 𝐴 ) ∈ Tarski )

Proof

Step Hyp Ref Expression
1 inawina ⊢ ( 𝐴 ∈ Inacc → 𝐴 ∈ Inaccw )
2 winaon ⊢ ( 𝐴 ∈ Inaccw → 𝐴 ∈ On )
3 winalim ⊢ ( 𝐴 ∈ Inaccw → Lim 𝐴 )
4 r1lim ⊢ ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) → ( 𝑅1 ‘ 𝐴 ) = ∪ 𝑦 ∈ 𝐴 ( 𝑅1 ‘ 𝑦 ) )
5 2 3 4 syl2anc ⊢ ( 𝐴 ∈ Inaccw → ( 𝑅1 ‘ 𝐴 ) = ∪ 𝑦 ∈ 𝐴 ( 𝑅1 ‘ 𝑦 ) )
6 5 eleq2d ⊢ ( 𝐴 ∈ Inaccw → ( 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ↔ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ( 𝑅1 ‘ 𝑦 ) ) )
7 eliun ⊢ ( 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ( 𝑅1 ‘ 𝑦 ) ↔ ∃ 𝑦 ∈ 𝐴 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) )
8 6 7 bitrdi ⊢ ( 𝐴 ∈ Inaccw → ( 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ↔ ∃ 𝑦 ∈ 𝐴 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) )
9 onelon ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ On )
10 2 9 sylan ⊢ ( ( 𝐴 ∈ Inaccw ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ On )
11 r1pw ⊢ ( 𝑦 ∈ On → ( 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ↔ 𝒫 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) ) )
12 10 11 syl ⊢ ( ( 𝐴 ∈ Inaccw ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ↔ 𝒫 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) ) )
13 limsuc ⊢ ( Lim 𝐴 → ( 𝑦 ∈ 𝐴 ↔ suc 𝑦 ∈ 𝐴 ) )
14 3 13 syl ⊢ ( 𝐴 ∈ Inaccw → ( 𝑦 ∈ 𝐴 ↔ suc 𝑦 ∈ 𝐴 ) )
15 r1ord2 ⊢ ( 𝐴 ∈ On → ( suc 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ suc 𝑦 ) ⊆ ( 𝑅1 ‘ 𝐴 ) ) )
16 2 15 syl ⊢ ( 𝐴 ∈ Inaccw → ( suc 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ suc 𝑦 ) ⊆ ( 𝑅1 ‘ 𝐴 ) ) )
17 14 16 sylbid ⊢ ( 𝐴 ∈ Inaccw → ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ suc 𝑦 ) ⊆ ( 𝑅1 ‘ 𝐴 ) ) )
18 17 imp ⊢ ( ( 𝐴 ∈ Inaccw ∧ 𝑦 ∈ 𝐴 ) → ( 𝑅1 ‘ suc 𝑦 ) ⊆ ( 𝑅1 ‘ 𝐴 ) )
19 18 sseld ⊢ ( ( 𝐴 ∈ Inaccw ∧ 𝑦 ∈ 𝐴 ) → ( 𝒫 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) → 𝒫 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) )
20 12 19 sylbid ⊢ ( ( 𝐴 ∈ Inaccw ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) → 𝒫 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) )
21 20 rexlimdva ⊢ ( 𝐴 ∈ Inaccw → ( ∃ 𝑦 ∈ 𝐴 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) → 𝒫 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) )
22 8 21 sylbid ⊢ ( 𝐴 ∈ Inaccw → ( 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) → 𝒫 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) )
23 1 22 syl ⊢ ( 𝐴 ∈ Inacc → ( 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) → 𝒫 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) )
24 23 imp ⊢ ( ( 𝐴 ∈ Inacc ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) → 𝒫 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) )
25 elssuni ⊢ ( 𝒫 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) → 𝒫 𝑥 ⊆ ∪ ( 𝑅1 ‘ 𝐴 ) )
26 r1tr2 ⊢ ∪ ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ 𝐴 )
27 25 26 sstrdi ⊢ ( 𝒫 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) → 𝒫 𝑥 ⊆ ( 𝑅1 ‘ 𝐴 ) )
28 24 27 jccil ⊢ ( ( 𝐴 ∈ Inacc ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) → ( 𝒫 𝑥 ⊆ ( 𝑅1 ‘ 𝐴 ) ∧ 𝒫 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) )
29 28 ralrimiva ⊢ ( 𝐴 ∈ Inacc → ∀ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ( 𝒫 𝑥 ⊆ ( 𝑅1 ‘ 𝐴 ) ∧ 𝒫 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) )
30 1 2 syl ⊢ ( 𝐴 ∈ Inacc → 𝐴 ∈ On )
31 r1suc ⊢ ( 𝐴 ∈ On → ( 𝑅1 ‘ suc 𝐴 ) = 𝒫 ( 𝑅1 ‘ 𝐴 ) )
32 31 eleq2d ⊢ ( 𝐴 ∈ On → ( 𝑥 ∈ ( 𝑅1 ‘ suc 𝐴 ) ↔ 𝑥 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ) )
33 30 32 syl ⊢ ( 𝐴 ∈ Inacc → ( 𝑥 ∈ ( 𝑅1 ‘ suc 𝐴 ) ↔ 𝑥 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ) )
34 rankr1ai ⊢ ( 𝑥 ∈ ( 𝑅1 ‘ suc 𝐴 ) → ( rank ‘ 𝑥 ) ∈ suc 𝐴 )
35 33 34 syl6bir ⊢ ( 𝐴 ∈ Inacc → ( 𝑥 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) → ( rank ‘ 𝑥 ) ∈ suc 𝐴 ) )
36 35 imp ⊢ ( ( 𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ) → ( rank ‘ 𝑥 ) ∈ suc 𝐴 )
37 fvex ⊢ ( rank ‘ 𝑥 ) ∈ V
38 37 elsuc ⊢ ( ( rank ‘ 𝑥 ) ∈ suc 𝐴 ↔ ( ( rank ‘ 𝑥 ) ∈ 𝐴 ∨ ( rank ‘ 𝑥 ) = 𝐴 ) )
39 36 38 sylib ⊢ ( ( 𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ) → ( ( rank ‘ 𝑥 ) ∈ 𝐴 ∨ ( rank ‘ 𝑥 ) = 𝐴 ) )
40 39 orcomd ⊢ ( ( 𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ) → ( ( rank ‘ 𝑥 ) = 𝐴 ∨ ( rank ‘ 𝑥 ) ∈ 𝐴 ) )
41 fvex ⊢ ( 𝑅1 ‘ 𝐴 ) ∈ V
42 elpwi ⊢ ( 𝑥 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) → 𝑥 ⊆ ( 𝑅1 ‘ 𝐴 ) )
43 42 ad2antlr ⊢ ( ( ( 𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ) ∧ ( rank ‘ 𝑥 ) = 𝐴 ) → 𝑥 ⊆ ( 𝑅1 ‘ 𝐴 ) )
44 ssdomg ⊢ ( ( 𝑅1 ‘ 𝐴 ) ∈ V → ( 𝑥 ⊆ ( 𝑅1 ‘ 𝐴 ) → 𝑥 ≼ ( 𝑅1 ‘ 𝐴 ) ) )
45 41 43 44 mpsyl ⊢ ( ( ( 𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ) ∧ ( rank ‘ 𝑥 ) = 𝐴 ) → 𝑥 ≼ ( 𝑅1 ‘ 𝐴 ) )
46 rankcf ⊢ ¬ 𝑥 ≺ ( cf ‘ ( rank ‘ 𝑥 ) )
47 fveq2 ⊢ ( ( rank ‘ 𝑥 ) = 𝐴 → ( cf ‘ ( rank ‘ 𝑥 ) ) = ( cf ‘ 𝐴 ) )
48 elina ⊢ ( 𝐴 ∈ Inacc ↔ ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 ) )
49 48 simp2bi ⊢ ( 𝐴 ∈ Inacc → ( cf ‘ 𝐴 ) = 𝐴 )
50 47 49 sylan9eqr ⊢ ( ( 𝐴 ∈ Inacc ∧ ( rank ‘ 𝑥 ) = 𝐴 ) → ( cf ‘ ( rank ‘ 𝑥 ) ) = 𝐴 )
51 50 breq2d ⊢ ( ( 𝐴 ∈ Inacc ∧ ( rank ‘ 𝑥 ) = 𝐴 ) → ( 𝑥 ≺ ( cf ‘ ( rank ‘ 𝑥 ) ) ↔ 𝑥 ≺ 𝐴 ) )
52 46 51 mtbii ⊢ ( ( 𝐴 ∈ Inacc ∧ ( rank ‘ 𝑥 ) = 𝐴 ) → ¬ 𝑥 ≺ 𝐴 )
53 inar1 ⊢ ( 𝐴 ∈ Inacc → ( 𝑅1 ‘ 𝐴 ) ≈ 𝐴 )
54 sdomentr ⊢ ( ( 𝑥 ≺ ( 𝑅1 ‘ 𝐴 ) ∧ ( 𝑅1 ‘ 𝐴 ) ≈ 𝐴 ) → 𝑥 ≺ 𝐴 )
55 54 expcom ⊢ ( ( 𝑅1 ‘ 𝐴 ) ≈ 𝐴 → ( 𝑥 ≺ ( 𝑅1 ‘ 𝐴 ) → 𝑥 ≺ 𝐴 ) )
56 53 55 syl ⊢ ( 𝐴 ∈ Inacc → ( 𝑥 ≺ ( 𝑅1 ‘ 𝐴 ) → 𝑥 ≺ 𝐴 ) )
57 56 adantr ⊢ ( ( 𝐴 ∈ Inacc ∧ ( rank ‘ 𝑥 ) = 𝐴 ) → ( 𝑥 ≺ ( 𝑅1 ‘ 𝐴 ) → 𝑥 ≺ 𝐴 ) )
58 52 57 mtod ⊢ ( ( 𝐴 ∈ Inacc ∧ ( rank ‘ 𝑥 ) = 𝐴 ) → ¬ 𝑥 ≺ ( 𝑅1 ‘ 𝐴 ) )
59 58 adantlr ⊢ ( ( ( 𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ) ∧ ( rank ‘ 𝑥 ) = 𝐴 ) → ¬ 𝑥 ≺ ( 𝑅1 ‘ 𝐴 ) )
60 bren2 ⊢ ( 𝑥 ≈ ( 𝑅1 ‘ 𝐴 ) ↔ ( 𝑥 ≼ ( 𝑅1 ‘ 𝐴 ) ∧ ¬ 𝑥 ≺ ( 𝑅1 ‘ 𝐴 ) ) )
61 45 59 60 sylanbrc ⊢ ( ( ( 𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ) ∧ ( rank ‘ 𝑥 ) = 𝐴 ) → 𝑥 ≈ ( 𝑅1 ‘ 𝐴 ) )
62 61 ex ⊢ ( ( 𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ) → ( ( rank ‘ 𝑥 ) = 𝐴 → 𝑥 ≈ ( 𝑅1 ‘ 𝐴 ) ) )
63 r1elwf ⊢ ( 𝑥 ∈ ( 𝑅1 ‘ suc 𝐴 ) → 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
64 33 63 syl6bir ⊢ ( 𝐴 ∈ Inacc → ( 𝑥 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) → 𝑥 ∈ ∪ ( 𝑅1 “ On ) ) )
65 64 imp ⊢ ( ( 𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ) → 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
66 r1fnon ⊢ 𝑅1 Fn On
67 66 fndmi ⊢ dom 𝑅1 = On
68 30 67 eleqtrrdi ⊢ ( 𝐴 ∈ Inacc → 𝐴 ∈ dom 𝑅1 )
69 68 adantr ⊢ ( ( 𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ) → 𝐴 ∈ dom 𝑅1 )
70 rankr1ag ⊢ ( ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐴 ∈ dom 𝑅1 ) → ( 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ↔ ( rank ‘ 𝑥 ) ∈ 𝐴 ) )
71 65 69 70 syl2anc ⊢ ( ( 𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ) → ( 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ↔ ( rank ‘ 𝑥 ) ∈ 𝐴 ) )
72 71 biimprd ⊢ ( ( 𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ) → ( ( rank ‘ 𝑥 ) ∈ 𝐴 → 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) )
73 62 72 orim12d ⊢ ( ( 𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ) → ( ( ( rank ‘ 𝑥 ) = 𝐴 ∨ ( rank ‘ 𝑥 ) ∈ 𝐴 ) → ( 𝑥 ≈ ( 𝑅1 ‘ 𝐴 ) ∨ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ) )
74 40 73 mpd ⊢ ( ( 𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ) → ( 𝑥 ≈ ( 𝑅1 ‘ 𝐴 ) ∨ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) )
75 74 ralrimiva ⊢ ( 𝐴 ∈ Inacc → ∀ 𝑥 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ( 𝑥 ≈ ( 𝑅1 ‘ 𝐴 ) ∨ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) )
76 eltsk2g ⊢ ( ( 𝑅1 ‘ 𝐴 ) ∈ V → ( ( 𝑅1 ‘ 𝐴 ) ∈ Tarski ↔ ( ∀ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ( 𝒫 𝑥 ⊆ ( 𝑅1 ‘ 𝐴 ) ∧ 𝒫 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ∧ ∀ 𝑥 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ( 𝑥 ≈ ( 𝑅1 ‘ 𝐴 ) ∨ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ) ) )
77 41 76 ax-mp ⊢ ( ( 𝑅1 ‘ 𝐴 ) ∈ Tarski ↔ ( ∀ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ( 𝒫 𝑥 ⊆ ( 𝑅1 ‘ 𝐴 ) ∧ 𝒫 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ∧ ∀ 𝑥 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ( 𝑥 ≈ ( 𝑅1 ‘ 𝐴 ) ∨ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ) )
78 29 75 77 sylanbrc ⊢ ( 𝐴 ∈ Inacc → ( 𝑅1 ‘ 𝐴 ) ∈ Tarski )