Step | Hyp | Ref
| Expression |
1 | | inawina 10101 |
. . . . . 6
⊢ (𝐴 ∈ Inacc → 𝐴 ∈
Inaccw) |
2 | | winaon 10099 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Inaccw →
𝐴 ∈
On) |
3 | | winalim 10106 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Inaccw →
Lim 𝐴) |
4 | | r1lim 9185 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ Lim 𝐴) →
(𝑅1‘𝐴) = ∪
𝑦 ∈ 𝐴 (𝑅1‘𝑦)) |
5 | 2, 3, 4 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝐴 ∈ Inaccw →
(𝑅1‘𝐴) = ∪
𝑦 ∈ 𝐴 (𝑅1‘𝑦)) |
6 | 5 | eleq2d 2875 |
. . . . . . . 8
⊢ (𝐴 ∈ Inaccw →
(𝑥 ∈
(𝑅1‘𝐴) ↔ 𝑥 ∈ ∪
𝑦 ∈ 𝐴 (𝑅1‘𝑦))) |
7 | | eliun 4885 |
. . . . . . . 8
⊢ (𝑥 ∈ ∪ 𝑦 ∈ 𝐴 (𝑅1‘𝑦) ↔ ∃𝑦 ∈ 𝐴 𝑥 ∈ (𝑅1‘𝑦)) |
8 | 6, 7 | syl6bb 290 |
. . . . . . 7
⊢ (𝐴 ∈ Inaccw →
(𝑥 ∈
(𝑅1‘𝐴) ↔ ∃𝑦 ∈ 𝐴 𝑥 ∈ (𝑅1‘𝑦))) |
9 | | onelon 6184 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ On) |
10 | 2, 9 | sylan 583 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Inaccw ∧
𝑦 ∈ 𝐴) → 𝑦 ∈ On) |
11 | | r1pw 9258 |
. . . . . . . . . 10
⊢ (𝑦 ∈ On → (𝑥 ∈
(𝑅1‘𝑦) ↔ 𝒫 𝑥 ∈ (𝑅1‘suc
𝑦))) |
12 | 10, 11 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Inaccw ∧
𝑦 ∈ 𝐴) → (𝑥 ∈ (𝑅1‘𝑦) ↔ 𝒫 𝑥 ∈
(𝑅1‘suc 𝑦))) |
13 | | limsuc 7544 |
. . . . . . . . . . . . 13
⊢ (Lim
𝐴 → (𝑦 ∈ 𝐴 ↔ suc 𝑦 ∈ 𝐴)) |
14 | 3, 13 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Inaccw →
(𝑦 ∈ 𝐴 ↔ suc 𝑦 ∈ 𝐴)) |
15 | | r1ord2 9194 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ On → (suc 𝑦 ∈ 𝐴 → (𝑅1‘suc
𝑦) ⊆
(𝑅1‘𝐴))) |
16 | 2, 15 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Inaccw →
(suc 𝑦 ∈ 𝐴 →
(𝑅1‘suc 𝑦) ⊆ (𝑅1‘𝐴))) |
17 | 14, 16 | sylbid 243 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Inaccw →
(𝑦 ∈ 𝐴 → (𝑅1‘suc
𝑦) ⊆
(𝑅1‘𝐴))) |
18 | 17 | imp 410 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Inaccw ∧
𝑦 ∈ 𝐴) → (𝑅1‘suc
𝑦) ⊆
(𝑅1‘𝐴)) |
19 | 18 | sseld 3914 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Inaccw ∧
𝑦 ∈ 𝐴) → (𝒫 𝑥 ∈ (𝑅1‘suc
𝑦) → 𝒫 𝑥 ∈
(𝑅1‘𝐴))) |
20 | 12, 19 | sylbid 243 |
. . . . . . . 8
⊢ ((𝐴 ∈ Inaccw ∧
𝑦 ∈ 𝐴) → (𝑥 ∈ (𝑅1‘𝑦) → 𝒫 𝑥 ∈
(𝑅1‘𝐴))) |
21 | 20 | rexlimdva 3243 |
. . . . . . 7
⊢ (𝐴 ∈ Inaccw →
(∃𝑦 ∈ 𝐴 𝑥 ∈ (𝑅1‘𝑦) → 𝒫 𝑥 ∈
(𝑅1‘𝐴))) |
22 | 8, 21 | sylbid 243 |
. . . . . 6
⊢ (𝐴 ∈ Inaccw →
(𝑥 ∈
(𝑅1‘𝐴) → 𝒫 𝑥 ∈ (𝑅1‘𝐴))) |
23 | 1, 22 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ Inacc → (𝑥 ∈
(𝑅1‘𝐴) → 𝒫 𝑥 ∈ (𝑅1‘𝐴))) |
24 | 23 | imp 410 |
. . . 4
⊢ ((𝐴 ∈ Inacc ∧ 𝑥 ∈
(𝑅1‘𝐴)) → 𝒫 𝑥 ∈ (𝑅1‘𝐴)) |
25 | | elssuni 4830 |
. . . . 5
⊢
(𝒫 𝑥 ∈
(𝑅1‘𝐴) → 𝒫 𝑥 ⊆ ∪
(𝑅1‘𝐴)) |
26 | | r1tr2 9190 |
. . . . 5
⊢ ∪ (𝑅1‘𝐴) ⊆ (𝑅1‘𝐴) |
27 | 25, 26 | sstrdi 3927 |
. . . 4
⊢
(𝒫 𝑥 ∈
(𝑅1‘𝐴) → 𝒫 𝑥 ⊆ (𝑅1‘𝐴)) |
28 | 24, 27 | jccil 526 |
. . 3
⊢ ((𝐴 ∈ Inacc ∧ 𝑥 ∈
(𝑅1‘𝐴)) → (𝒫 𝑥 ⊆ (𝑅1‘𝐴) ∧ 𝒫 𝑥 ∈
(𝑅1‘𝐴))) |
29 | 28 | ralrimiva 3149 |
. 2
⊢ (𝐴 ∈ Inacc →
∀𝑥 ∈
(𝑅1‘𝐴)(𝒫 𝑥 ⊆ (𝑅1‘𝐴) ∧ 𝒫 𝑥 ∈
(𝑅1‘𝐴))) |
30 | 1, 2 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ Inacc → 𝐴 ∈ On) |
31 | | r1suc 9183 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On →
(𝑅1‘suc 𝐴) = 𝒫
(𝑅1‘𝐴)) |
32 | 31 | eleq2d 2875 |
. . . . . . . . 9
⊢ (𝐴 ∈ On → (𝑥 ∈
(𝑅1‘suc 𝐴) ↔ 𝑥 ∈ 𝒫
(𝑅1‘𝐴))) |
33 | 30, 32 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ Inacc → (𝑥 ∈
(𝑅1‘suc 𝐴) ↔ 𝑥 ∈ 𝒫
(𝑅1‘𝐴))) |
34 | | rankr1ai 9211 |
. . . . . . . 8
⊢ (𝑥 ∈
(𝑅1‘suc 𝐴) → (rank‘𝑥) ∈ suc 𝐴) |
35 | 33, 34 | syl6bir 257 |
. . . . . . 7
⊢ (𝐴 ∈ Inacc → (𝑥 ∈ 𝒫
(𝑅1‘𝐴) → (rank‘𝑥) ∈ suc 𝐴)) |
36 | 35 | imp 410 |
. . . . . 6
⊢ ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫
(𝑅1‘𝐴)) → (rank‘𝑥) ∈ suc 𝐴) |
37 | | fvex 6658 |
. . . . . . 7
⊢
(rank‘𝑥)
∈ V |
38 | 37 | elsuc 6228 |
. . . . . 6
⊢
((rank‘𝑥)
∈ suc 𝐴 ↔
((rank‘𝑥) ∈
𝐴 ∨ (rank‘𝑥) = 𝐴)) |
39 | 36, 38 | sylib 221 |
. . . . 5
⊢ ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫
(𝑅1‘𝐴)) → ((rank‘𝑥) ∈ 𝐴 ∨ (rank‘𝑥) = 𝐴)) |
40 | 39 | orcomd 868 |
. . . 4
⊢ ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫
(𝑅1‘𝐴)) → ((rank‘𝑥) = 𝐴 ∨ (rank‘𝑥) ∈ 𝐴)) |
41 | | fvex 6658 |
. . . . . . . 8
⊢
(𝑅1‘𝐴) ∈ V |
42 | | elpwi 4506 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝒫
(𝑅1‘𝐴) → 𝑥 ⊆ (𝑅1‘𝐴)) |
43 | 42 | ad2antlr 726 |
. . . . . . . 8
⊢ (((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫
(𝑅1‘𝐴)) ∧ (rank‘𝑥) = 𝐴) → 𝑥 ⊆ (𝑅1‘𝐴)) |
44 | | ssdomg 8538 |
. . . . . . . 8
⊢
((𝑅1‘𝐴) ∈ V → (𝑥 ⊆ (𝑅1‘𝐴) → 𝑥 ≼ (𝑅1‘𝐴))) |
45 | 41, 43, 44 | mpsyl 68 |
. . . . . . 7
⊢ (((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫
(𝑅1‘𝐴)) ∧ (rank‘𝑥) = 𝐴) → 𝑥 ≼ (𝑅1‘𝐴)) |
46 | | rankcf 10188 |
. . . . . . . . . 10
⊢ ¬
𝑥 ≺
(cf‘(rank‘𝑥)) |
47 | | fveq2 6645 |
. . . . . . . . . . . 12
⊢
((rank‘𝑥) =
𝐴 →
(cf‘(rank‘𝑥)) =
(cf‘𝐴)) |
48 | | elina 10098 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Inacc ↔ (𝐴 ≠ ∅ ∧
(cf‘𝐴) = 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴)) |
49 | 48 | simp2bi 1143 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Inacc →
(cf‘𝐴) = 𝐴) |
50 | 47, 49 | sylan9eqr 2855 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ Inacc ∧
(rank‘𝑥) = 𝐴) →
(cf‘(rank‘𝑥)) =
𝐴) |
51 | 50 | breq2d 5042 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Inacc ∧
(rank‘𝑥) = 𝐴) → (𝑥 ≺ (cf‘(rank‘𝑥)) ↔ 𝑥 ≺ 𝐴)) |
52 | 46, 51 | mtbii 329 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Inacc ∧
(rank‘𝑥) = 𝐴) → ¬ 𝑥 ≺ 𝐴) |
53 | | inar1 10186 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Inacc →
(𝑅1‘𝐴) ≈ 𝐴) |
54 | | sdomentr 8635 |
. . . . . . . . . . . 12
⊢ ((𝑥 ≺
(𝑅1‘𝐴) ∧ (𝑅1‘𝐴) ≈ 𝐴) → 𝑥 ≺ 𝐴) |
55 | 54 | expcom 417 |
. . . . . . . . . . 11
⊢
((𝑅1‘𝐴) ≈ 𝐴 → (𝑥 ≺ (𝑅1‘𝐴) → 𝑥 ≺ 𝐴)) |
56 | 53, 55 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Inacc → (𝑥 ≺
(𝑅1‘𝐴) → 𝑥 ≺ 𝐴)) |
57 | 56 | adantr 484 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Inacc ∧
(rank‘𝑥) = 𝐴) → (𝑥 ≺ (𝑅1‘𝐴) → 𝑥 ≺ 𝐴)) |
58 | 52, 57 | mtod 201 |
. . . . . . . 8
⊢ ((𝐴 ∈ Inacc ∧
(rank‘𝑥) = 𝐴) → ¬ 𝑥 ≺
(𝑅1‘𝐴)) |
59 | 58 | adantlr 714 |
. . . . . . 7
⊢ (((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫
(𝑅1‘𝐴)) ∧ (rank‘𝑥) = 𝐴) → ¬ 𝑥 ≺ (𝑅1‘𝐴)) |
60 | | bren2 8523 |
. . . . . . 7
⊢ (𝑥 ≈
(𝑅1‘𝐴) ↔ (𝑥 ≼ (𝑅1‘𝐴) ∧ ¬ 𝑥 ≺ (𝑅1‘𝐴))) |
61 | 45, 59, 60 | sylanbrc 586 |
. . . . . 6
⊢ (((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫
(𝑅1‘𝐴)) ∧ (rank‘𝑥) = 𝐴) → 𝑥 ≈ (𝑅1‘𝐴)) |
62 | 61 | ex 416 |
. . . . 5
⊢ ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫
(𝑅1‘𝐴)) → ((rank‘𝑥) = 𝐴 → 𝑥 ≈ (𝑅1‘𝐴))) |
63 | | r1elwf 9209 |
. . . . . . . . 9
⊢ (𝑥 ∈
(𝑅1‘suc 𝐴) → 𝑥 ∈ ∪
(𝑅1 “ On)) |
64 | 33, 63 | syl6bir 257 |
. . . . . . . 8
⊢ (𝐴 ∈ Inacc → (𝑥 ∈ 𝒫
(𝑅1‘𝐴) → 𝑥 ∈ ∪
(𝑅1 “ On))) |
65 | 64 | imp 410 |
. . . . . . 7
⊢ ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫
(𝑅1‘𝐴)) → 𝑥 ∈ ∪
(𝑅1 “ On)) |
66 | | r1fnon 9180 |
. . . . . . . . . 10
⊢
𝑅1 Fn On |
67 | 66 | fndmi 6426 |
. . . . . . . . 9
⊢ dom
𝑅1 = On |
68 | 30, 67 | eleqtrrdi 2901 |
. . . . . . . 8
⊢ (𝐴 ∈ Inacc → 𝐴 ∈ dom
𝑅1) |
69 | 68 | adantr 484 |
. . . . . . 7
⊢ ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫
(𝑅1‘𝐴)) → 𝐴 ∈ dom
𝑅1) |
70 | | rankr1ag 9215 |
. . . . . . 7
⊢ ((𝑥 ∈ ∪ (𝑅1 “ On) ∧ 𝐴 ∈ dom
𝑅1) → (𝑥 ∈ (𝑅1‘𝐴) ↔ (rank‘𝑥) ∈ 𝐴)) |
71 | 65, 69, 70 | syl2anc 587 |
. . . . . 6
⊢ ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫
(𝑅1‘𝐴)) → (𝑥 ∈ (𝑅1‘𝐴) ↔ (rank‘𝑥) ∈ 𝐴)) |
72 | 71 | biimprd 251 |
. . . . 5
⊢ ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫
(𝑅1‘𝐴)) → ((rank‘𝑥) ∈ 𝐴 → 𝑥 ∈ (𝑅1‘𝐴))) |
73 | 62, 72 | orim12d 962 |
. . . 4
⊢ ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫
(𝑅1‘𝐴)) → (((rank‘𝑥) = 𝐴 ∨ (rank‘𝑥) ∈ 𝐴) → (𝑥 ≈ (𝑅1‘𝐴) ∨ 𝑥 ∈ (𝑅1‘𝐴)))) |
74 | 40, 73 | mpd 15 |
. . 3
⊢ ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫
(𝑅1‘𝐴)) → (𝑥 ≈ (𝑅1‘𝐴) ∨ 𝑥 ∈ (𝑅1‘𝐴))) |
75 | 74 | ralrimiva 3149 |
. 2
⊢ (𝐴 ∈ Inacc →
∀𝑥 ∈ 𝒫
(𝑅1‘𝐴)(𝑥 ≈ (𝑅1‘𝐴) ∨ 𝑥 ∈ (𝑅1‘𝐴))) |
76 | | eltsk2g 10162 |
. . 3
⊢
((𝑅1‘𝐴) ∈ V →
((𝑅1‘𝐴) ∈ Tarski ↔ (∀𝑥 ∈
(𝑅1‘𝐴)(𝒫 𝑥 ⊆ (𝑅1‘𝐴) ∧ 𝒫 𝑥 ∈
(𝑅1‘𝐴)) ∧ ∀𝑥 ∈ 𝒫
(𝑅1‘𝐴)(𝑥 ≈ (𝑅1‘𝐴) ∨ 𝑥 ∈ (𝑅1‘𝐴))))) |
77 | 41, 76 | ax-mp 5 |
. 2
⊢
((𝑅1‘𝐴) ∈ Tarski ↔ (∀𝑥 ∈
(𝑅1‘𝐴)(𝒫 𝑥 ⊆ (𝑅1‘𝐴) ∧ 𝒫 𝑥 ∈
(𝑅1‘𝐴)) ∧ ∀𝑥 ∈ 𝒫
(𝑅1‘𝐴)(𝑥 ≈ (𝑅1‘𝐴) ∨ 𝑥 ∈ (𝑅1‘𝐴)))) |
78 | 29, 75, 77 | sylanbrc 586 |
1
⊢ (𝐴 ∈ Inacc →
(𝑅1‘𝐴) ∈ Tarski) |