Step | Hyp | Ref
| Expression |
1 | | simpr 487 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) →
(𝑅1‘𝐴) ∈ WUni) |
2 | 1 | wun0 10134 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) → ∅
∈ (𝑅1‘𝐴)) |
3 | | elfvdm 6696 |
. . . . . 6
⊢ (∅
∈ (𝑅1‘𝐴) → 𝐴 ∈ dom
𝑅1) |
4 | 2, 3 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) → 𝐴 ∈ dom
𝑅1) |
5 | | r1fnon 9190 |
. . . . . 6
⊢
𝑅1 Fn On |
6 | | fndm 6449 |
. . . . . 6
⊢
(𝑅1 Fn On → dom 𝑅1 =
On) |
7 | 5, 6 | ax-mp 5 |
. . . . 5
⊢ dom
𝑅1 = On |
8 | 4, 7 | eleqtrdi 2923 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) → 𝐴 ∈ On) |
9 | | eloni 6195 |
. . . 4
⊢ (𝐴 ∈ On → Ord 𝐴) |
10 | 8, 9 | syl 17 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) → Ord 𝐴) |
11 | | n0i 4298 |
. . . . . 6
⊢ (∅
∈ (𝑅1‘𝐴) → ¬
(𝑅1‘𝐴) = ∅) |
12 | 2, 11 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) → ¬
(𝑅1‘𝐴) = ∅) |
13 | | fveq2 6664 |
. . . . . 6
⊢ (𝐴 = ∅ →
(𝑅1‘𝐴) =
(𝑅1‘∅)) |
14 | | r10 9191 |
. . . . . 6
⊢
(𝑅1‘∅) = ∅ |
15 | 13, 14 | syl6eq 2872 |
. . . . 5
⊢ (𝐴 = ∅ →
(𝑅1‘𝐴) = ∅) |
16 | 12, 15 | nsyl 142 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) → ¬
𝐴 =
∅) |
17 | | suceloni 7522 |
. . . . . . . 8
⊢ (𝐴 ∈ On → suc 𝐴 ∈ On) |
18 | 8, 17 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) → suc 𝐴 ∈ On) |
19 | | sucidg 6263 |
. . . . . . . 8
⊢ (𝐴 ∈ On → 𝐴 ∈ suc 𝐴) |
20 | 8, 19 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) → 𝐴 ∈ suc 𝐴) |
21 | | r1ord 9203 |
. . . . . . 7
⊢ (suc
𝐴 ∈ On → (𝐴 ∈ suc 𝐴 → (𝑅1‘𝐴) ∈
(𝑅1‘suc 𝐴))) |
22 | 18, 20, 21 | sylc 65 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) →
(𝑅1‘𝐴) ∈ (𝑅1‘suc
𝐴)) |
23 | | r1elwf 9219 |
. . . . . 6
⊢
((𝑅1‘𝐴) ∈ (𝑅1‘suc
𝐴) →
(𝑅1‘𝐴) ∈ ∪
(𝑅1 “ On)) |
24 | | wfelirr 9248 |
. . . . . 6
⊢
((𝑅1‘𝐴) ∈ ∪
(𝑅1 “ On) → ¬
(𝑅1‘𝐴) ∈ (𝑅1‘𝐴)) |
25 | 22, 23, 24 | 3syl 18 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) → ¬
(𝑅1‘𝐴) ∈ (𝑅1‘𝐴)) |
26 | | simprr 771 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) ∧ (𝑥 ∈ On ∧ 𝐴 = suc 𝑥)) → 𝐴 = suc 𝑥) |
27 | 26 | fveq2d 6668 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) ∧ (𝑥 ∈ On ∧ 𝐴 = suc 𝑥)) → (𝑅1‘𝐴) =
(𝑅1‘suc 𝑥)) |
28 | | r1suc 9193 |
. . . . . . . . 9
⊢ (𝑥 ∈ On →
(𝑅1‘suc 𝑥) = 𝒫
(𝑅1‘𝑥)) |
29 | 28 | ad2antrl 726 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) ∧ (𝑥 ∈ On ∧ 𝐴 = suc 𝑥)) → (𝑅1‘suc
𝑥) = 𝒫
(𝑅1‘𝑥)) |
30 | 27, 29 | eqtrd 2856 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) ∧ (𝑥 ∈ On ∧ 𝐴 = suc 𝑥)) → (𝑅1‘𝐴) = 𝒫
(𝑅1‘𝑥)) |
31 | | simplr 767 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) ∧ (𝑥 ∈ On ∧ 𝐴 = suc 𝑥)) → (𝑅1‘𝐴) ∈ WUni) |
32 | 8 | adantr 483 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) ∧ (𝑥 ∈ On ∧ 𝐴 = suc 𝑥)) → 𝐴 ∈ On) |
33 | | sucidg 6263 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ On → 𝑥 ∈ suc 𝑥) |
34 | 33 | ad2antrl 726 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) ∧ (𝑥 ∈ On ∧ 𝐴 = suc 𝑥)) → 𝑥 ∈ suc 𝑥) |
35 | 34, 26 | eleqtrrd 2916 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) ∧ (𝑥 ∈ On ∧ 𝐴 = suc 𝑥)) → 𝑥 ∈ 𝐴) |
36 | | r1ord 9203 |
. . . . . . . . 9
⊢ (𝐴 ∈ On → (𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ∈
(𝑅1‘𝐴))) |
37 | 32, 35, 36 | sylc 65 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) ∧ (𝑥 ∈ On ∧ 𝐴 = suc 𝑥)) → (𝑅1‘𝑥) ∈
(𝑅1‘𝐴)) |
38 | 31, 37 | wunpw 10123 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) ∧ (𝑥 ∈ On ∧ 𝐴 = suc 𝑥)) → 𝒫
(𝑅1‘𝑥) ∈ (𝑅1‘𝐴)) |
39 | 30, 38 | eqeltrd 2913 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) ∧ (𝑥 ∈ On ∧ 𝐴 = suc 𝑥)) → (𝑅1‘𝐴) ∈
(𝑅1‘𝐴)) |
40 | 39 | rexlimdvaa 3285 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) →
(∃𝑥 ∈ On 𝐴 = suc 𝑥 → (𝑅1‘𝐴) ∈
(𝑅1‘𝐴))) |
41 | 25, 40 | mtod 200 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) → ¬
∃𝑥 ∈ On 𝐴 = suc 𝑥) |
42 | | ioran 980 |
. . . 4
⊢ (¬
(𝐴 = ∅ ∨
∃𝑥 ∈ On 𝐴 = suc 𝑥) ↔ (¬ 𝐴 = ∅ ∧ ¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥)) |
43 | 16, 41, 42 | sylanbrc 585 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) → ¬
(𝐴 = ∅ ∨
∃𝑥 ∈ On 𝐴 = suc 𝑥)) |
44 | | dflim3 7556 |
. . 3
⊢ (Lim
𝐴 ↔ (Ord 𝐴 ∧ ¬ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥))) |
45 | 10, 43, 44 | sylanbrc 585 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) → Lim 𝐴) |
46 | | r1limwun 10152 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → (𝑅1‘𝐴) ∈ WUni) |
47 | 45, 46 | impbida 799 |
1
⊢ (𝐴 ∈ 𝑉 → ((𝑅1‘𝐴) ∈ WUni ↔ Lim 𝐴)) |