Step | Hyp | Ref
| Expression |
1 | | simpr 477 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) →
(𝑅1‘𝐴) ∈ WUni) |
2 | 1 | wun0 9940 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) → ∅
∈ (𝑅1‘𝐴)) |
3 | | elfvdm 6533 |
. . . . . 6
⊢ (∅
∈ (𝑅1‘𝐴) → 𝐴 ∈ dom
𝑅1) |
4 | 2, 3 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) → 𝐴 ∈ dom
𝑅1) |
5 | | r1fnon 8992 |
. . . . . 6
⊢
𝑅1 Fn On |
6 | | fndm 6290 |
. . . . . 6
⊢
(𝑅1 Fn On → dom 𝑅1 =
On) |
7 | 5, 6 | ax-mp 5 |
. . . . 5
⊢ dom
𝑅1 = On |
8 | 4, 7 | syl6eleq 2876 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) → 𝐴 ∈ On) |
9 | | eloni 6041 |
. . . 4
⊢ (𝐴 ∈ On → Ord 𝐴) |
10 | 8, 9 | syl 17 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) → Ord 𝐴) |
11 | | n0i 4187 |
. . . . . 6
⊢ (∅
∈ (𝑅1‘𝐴) → ¬
(𝑅1‘𝐴) = ∅) |
12 | 2, 11 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) → ¬
(𝑅1‘𝐴) = ∅) |
13 | | fveq2 6501 |
. . . . . 6
⊢ (𝐴 = ∅ →
(𝑅1‘𝐴) =
(𝑅1‘∅)) |
14 | | r10 8993 |
. . . . . 6
⊢
(𝑅1‘∅) = ∅ |
15 | 13, 14 | syl6eq 2830 |
. . . . 5
⊢ (𝐴 = ∅ →
(𝑅1‘𝐴) = ∅) |
16 | 12, 15 | nsyl 138 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) → ¬
𝐴 =
∅) |
17 | | suceloni 7346 |
. . . . . . . 8
⊢ (𝐴 ∈ On → suc 𝐴 ∈ On) |
18 | 8, 17 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) → suc 𝐴 ∈ On) |
19 | | sucidg 6109 |
. . . . . . . 8
⊢ (𝐴 ∈ On → 𝐴 ∈ suc 𝐴) |
20 | 8, 19 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) → 𝐴 ∈ suc 𝐴) |
21 | | r1ord 9005 |
. . . . . . 7
⊢ (suc
𝐴 ∈ On → (𝐴 ∈ suc 𝐴 → (𝑅1‘𝐴) ∈
(𝑅1‘suc 𝐴))) |
22 | 18, 20, 21 | sylc 65 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) →
(𝑅1‘𝐴) ∈ (𝑅1‘suc
𝐴)) |
23 | | r1elwf 9021 |
. . . . . 6
⊢
((𝑅1‘𝐴) ∈ (𝑅1‘suc
𝐴) →
(𝑅1‘𝐴) ∈ ∪
(𝑅1 “ On)) |
24 | | wfelirr 9050 |
. . . . . 6
⊢
((𝑅1‘𝐴) ∈ ∪
(𝑅1 “ On) → ¬
(𝑅1‘𝐴) ∈ (𝑅1‘𝐴)) |
25 | 22, 23, 24 | 3syl 18 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) → ¬
(𝑅1‘𝐴) ∈ (𝑅1‘𝐴)) |
26 | | simprr 760 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) ∧ (𝑥 ∈ On ∧ 𝐴 = suc 𝑥)) → 𝐴 = suc 𝑥) |
27 | 26 | fveq2d 6505 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) ∧ (𝑥 ∈ On ∧ 𝐴 = suc 𝑥)) → (𝑅1‘𝐴) =
(𝑅1‘suc 𝑥)) |
28 | | r1suc 8995 |
. . . . . . . . 9
⊢ (𝑥 ∈ On →
(𝑅1‘suc 𝑥) = 𝒫
(𝑅1‘𝑥)) |
29 | 28 | ad2antrl 715 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) ∧ (𝑥 ∈ On ∧ 𝐴 = suc 𝑥)) → (𝑅1‘suc
𝑥) = 𝒫
(𝑅1‘𝑥)) |
30 | 27, 29 | eqtrd 2814 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) ∧ (𝑥 ∈ On ∧ 𝐴 = suc 𝑥)) → (𝑅1‘𝐴) = 𝒫
(𝑅1‘𝑥)) |
31 | | simplr 756 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) ∧ (𝑥 ∈ On ∧ 𝐴 = suc 𝑥)) → (𝑅1‘𝐴) ∈ WUni) |
32 | 8 | adantr 473 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) ∧ (𝑥 ∈ On ∧ 𝐴 = suc 𝑥)) → 𝐴 ∈ On) |
33 | | sucidg 6109 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ On → 𝑥 ∈ suc 𝑥) |
34 | 33 | ad2antrl 715 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) ∧ (𝑥 ∈ On ∧ 𝐴 = suc 𝑥)) → 𝑥 ∈ suc 𝑥) |
35 | 34, 26 | eleqtrrd 2869 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) ∧ (𝑥 ∈ On ∧ 𝐴 = suc 𝑥)) → 𝑥 ∈ 𝐴) |
36 | | r1ord 9005 |
. . . . . . . . 9
⊢ (𝐴 ∈ On → (𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ∈
(𝑅1‘𝐴))) |
37 | 32, 35, 36 | sylc 65 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) ∧ (𝑥 ∈ On ∧ 𝐴 = suc 𝑥)) → (𝑅1‘𝑥) ∈
(𝑅1‘𝐴)) |
38 | 31, 37 | wunpw 9929 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) ∧ (𝑥 ∈ On ∧ 𝐴 = suc 𝑥)) → 𝒫
(𝑅1‘𝑥) ∈ (𝑅1‘𝐴)) |
39 | 30, 38 | eqeltrd 2866 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) ∧ (𝑥 ∈ On ∧ 𝐴 = suc 𝑥)) → (𝑅1‘𝐴) ∈
(𝑅1‘𝐴)) |
40 | 39 | rexlimdvaa 3230 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) →
(∃𝑥 ∈ On 𝐴 = suc 𝑥 → (𝑅1‘𝐴) ∈
(𝑅1‘𝐴))) |
41 | 25, 40 | mtod 190 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) → ¬
∃𝑥 ∈ On 𝐴 = suc 𝑥) |
42 | | ioran 966 |
. . . 4
⊢ (¬
(𝐴 = ∅ ∨
∃𝑥 ∈ On 𝐴 = suc 𝑥) ↔ (¬ 𝐴 = ∅ ∧ ¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥)) |
43 | 16, 41, 42 | sylanbrc 575 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) → ¬
(𝐴 = ∅ ∨
∃𝑥 ∈ On 𝐴 = suc 𝑥)) |
44 | | dflim3 7380 |
. . 3
⊢ (Lim
𝐴 ↔ (Ord 𝐴 ∧ ¬ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥))) |
45 | 10, 43, 44 | sylanbrc 575 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅1‘𝐴) ∈ WUni) → Lim 𝐴) |
46 | | r1limwun 9958 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → (𝑅1‘𝐴) ∈ WUni) |
47 | 45, 46 | impbida 788 |
1
⊢ (𝐴 ∈ 𝑉 → ((𝑅1‘𝐴) ∈ WUni ↔ Lim 𝐴)) |