Step | Hyp | Ref
| Expression |
1 | | eluni 4375 |
. . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ ∃𝑦(𝐴 ∈ 𝑦 ∧ 𝑦 ∈ (𝑅1 “
On))) |
2 | | r1funlim 8512 |
. . . . . . . 8
⊢ (Fun
𝑅1 ∧ Lim dom 𝑅1) |
3 | 2 | simpli 473 |
. . . . . . 7
⊢ Fun
𝑅1 |
4 | | fvelima 6158 |
. . . . . . 7
⊢ ((Fun
𝑅1 ∧ 𝑦 ∈ (𝑅1 “ On))
→ ∃𝑥 ∈ On
(𝑅1‘𝑥) = 𝑦) |
5 | 3, 4 | mpan 702 |
. . . . . 6
⊢ (𝑦 ∈ (𝑅1
“ On) → ∃𝑥
∈ On (𝑅1‘𝑥) = 𝑦) |
6 | | eleq2 2677 |
. . . . . . . . 9
⊢
((𝑅1‘𝑥) = 𝑦 → (𝐴 ∈ (𝑅1‘𝑥) ↔ 𝐴 ∈ 𝑦)) |
7 | 6 | biimprcd 239 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑦 → ((𝑅1‘𝑥) = 𝑦 → 𝐴 ∈ (𝑅1‘𝑥))) |
8 | | r1tr 8522 |
. . . . . . . . . . . 12
⊢ Tr
(𝑅1‘𝑥) |
9 | | trss 4689 |
. . . . . . . . . . . 12
⊢ (Tr
(𝑅1‘𝑥) → (𝐴 ∈ (𝑅1‘𝑥) → 𝐴 ⊆ (𝑅1‘𝑥))) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝐴 ∈
(𝑅1‘𝑥) → 𝐴 ⊆ (𝑅1‘𝑥)) |
11 | | elpwg 4116 |
. . . . . . . . . . 11
⊢ (𝐴 ∈
(𝑅1‘𝑥) → (𝐴 ∈ 𝒫
(𝑅1‘𝑥) ↔ 𝐴 ⊆ (𝑅1‘𝑥))) |
12 | 10, 11 | mpbird 246 |
. . . . . . . . . 10
⊢ (𝐴 ∈
(𝑅1‘𝑥) → 𝐴 ∈ 𝒫
(𝑅1‘𝑥)) |
13 | | elfvdm 6130 |
. . . . . . . . . . 11
⊢ (𝐴 ∈
(𝑅1‘𝑥) → 𝑥 ∈ dom
𝑅1) |
14 | | r1sucg 8515 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ dom
𝑅1 → (𝑅1‘suc 𝑥) = 𝒫
(𝑅1‘𝑥)) |
15 | 13, 14 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ∈
(𝑅1‘𝑥) → (𝑅1‘suc
𝑥) = 𝒫
(𝑅1‘𝑥)) |
16 | 12, 15 | eleqtrrd 2691 |
. . . . . . . . 9
⊢ (𝐴 ∈
(𝑅1‘𝑥) → 𝐴 ∈ (𝑅1‘suc
𝑥)) |
17 | 16 | a1i 11 |
. . . . . . . 8
⊢ (𝑥 ∈ On → (𝐴 ∈
(𝑅1‘𝑥) → 𝐴 ∈ (𝑅1‘suc
𝑥))) |
18 | 7, 17 | syl9 75 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑦 → (𝑥 ∈ On →
((𝑅1‘𝑥) = 𝑦 → 𝐴 ∈ (𝑅1‘suc
𝑥)))) |
19 | 18 | reximdvai 2998 |
. . . . . 6
⊢ (𝐴 ∈ 𝑦 → (∃𝑥 ∈ On (𝑅1‘𝑥) = 𝑦 → ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘suc
𝑥))) |
20 | 5, 19 | syl5 33 |
. . . . 5
⊢ (𝐴 ∈ 𝑦 → (𝑦 ∈ (𝑅1 “ On)
→ ∃𝑥 ∈ On
𝐴 ∈
(𝑅1‘suc 𝑥))) |
21 | 20 | imp 444 |
. . . 4
⊢ ((𝐴 ∈ 𝑦 ∧ 𝑦 ∈ (𝑅1 “ On))
→ ∃𝑥 ∈ On
𝐴 ∈
(𝑅1‘suc 𝑥)) |
22 | 21 | exlimiv 1845 |
. . 3
⊢
(∃𝑦(𝐴 ∈ 𝑦 ∧ 𝑦 ∈ (𝑅1 “ On))
→ ∃𝑥 ∈ On
𝐴 ∈
(𝑅1‘suc 𝑥)) |
23 | 1, 22 | sylbi 206 |
. 2
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘suc
𝑥)) |
24 | | elfvdm 6130 |
. . . . . 6
⊢ (𝐴 ∈
(𝑅1‘suc 𝑥) → suc 𝑥 ∈ dom
𝑅1) |
25 | | fvelrn 6260 |
. . . . . 6
⊢ ((Fun
𝑅1 ∧ suc 𝑥 ∈ dom 𝑅1) →
(𝑅1‘suc 𝑥) ∈ ran
𝑅1) |
26 | 3, 24, 25 | sylancr 694 |
. . . . 5
⊢ (𝐴 ∈
(𝑅1‘suc 𝑥) → (𝑅1‘suc
𝑥) ∈ ran
𝑅1) |
27 | | df-ima 5051 |
. . . . . 6
⊢
(𝑅1 “ On) = ran (𝑅1 ↾
On) |
28 | | funrel 5821 |
. . . . . . . . 9
⊢ (Fun
𝑅1 → Rel 𝑅1) |
29 | 3, 28 | ax-mp 5 |
. . . . . . . 8
⊢ Rel
𝑅1 |
30 | 2 | simpri 477 |
. . . . . . . . 9
⊢ Lim dom
𝑅1 |
31 | | limord 5701 |
. . . . . . . . 9
⊢ (Lim dom
𝑅1 → Ord dom 𝑅1) |
32 | | ordsson 6881 |
. . . . . . . . 9
⊢ (Ord dom
𝑅1 → dom 𝑅1 ⊆
On) |
33 | 30, 31, 32 | mp2b 10 |
. . . . . . . 8
⊢ dom
𝑅1 ⊆ On |
34 | | relssres 5357 |
. . . . . . . 8
⊢ ((Rel
𝑅1 ∧ dom 𝑅1 ⊆ On) →
(𝑅1 ↾ On) = 𝑅1) |
35 | 29, 33, 34 | mp2an 704 |
. . . . . . 7
⊢
(𝑅1 ↾ On) =
𝑅1 |
36 | 35 | rneqi 5273 |
. . . . . 6
⊢ ran
(𝑅1 ↾ On) = ran 𝑅1 |
37 | 27, 36 | eqtri 2632 |
. . . . 5
⊢
(𝑅1 “ On) = ran
𝑅1 |
38 | 26, 37 | syl6eleqr 2699 |
. . . 4
⊢ (𝐴 ∈
(𝑅1‘suc 𝑥) → (𝑅1‘suc
𝑥) ∈
(𝑅1 “ On)) |
39 | | elunii 4377 |
. . . 4
⊢ ((𝐴 ∈
(𝑅1‘suc 𝑥) ∧ (𝑅1‘suc
𝑥) ∈
(𝑅1 “ On)) → 𝐴 ∈ ∪
(𝑅1 “ On)) |
40 | 38, 39 | mpdan 699 |
. . 3
⊢ (𝐴 ∈
(𝑅1‘suc 𝑥) → 𝐴 ∈ ∪
(𝑅1 “ On)) |
41 | 40 | rexlimivw 3011 |
. 2
⊢
(∃𝑥 ∈ On
𝐴 ∈
(𝑅1‘suc 𝑥) → 𝐴 ∈ ∪
(𝑅1 “ On)) |
42 | 23, 41 | impbii 198 |
1
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘suc
𝑥)) |