| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eluni 4909 | . . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ ∃𝑦(𝐴 ∈ 𝑦 ∧ 𝑦 ∈ (𝑅1 “
On))) | 
| 2 |  | eleq2 2829 | . . . . . . . 8
⊢
((𝑅1‘𝑥) = 𝑦 → (𝐴 ∈ (𝑅1‘𝑥) ↔ 𝐴 ∈ 𝑦)) | 
| 3 | 2 | biimprcd 250 | . . . . . . 7
⊢ (𝐴 ∈ 𝑦 → ((𝑅1‘𝑥) = 𝑦 → 𝐴 ∈ (𝑅1‘𝑥))) | 
| 4 |  | r1tr 9817 | . . . . . . . . . . 11
⊢ Tr
(𝑅1‘𝑥) | 
| 5 |  | trss 5269 | . . . . . . . . . . 11
⊢ (Tr
(𝑅1‘𝑥) → (𝐴 ∈ (𝑅1‘𝑥) → 𝐴 ⊆ (𝑅1‘𝑥))) | 
| 6 | 4, 5 | ax-mp 5 | . . . . . . . . . 10
⊢ (𝐴 ∈
(𝑅1‘𝑥) → 𝐴 ⊆ (𝑅1‘𝑥)) | 
| 7 |  | elpwg 4602 | . . . . . . . . . 10
⊢ (𝐴 ∈
(𝑅1‘𝑥) → (𝐴 ∈ 𝒫
(𝑅1‘𝑥) ↔ 𝐴 ⊆ (𝑅1‘𝑥))) | 
| 8 | 6, 7 | mpbird 257 | . . . . . . . . 9
⊢ (𝐴 ∈
(𝑅1‘𝑥) → 𝐴 ∈ 𝒫
(𝑅1‘𝑥)) | 
| 9 |  | elfvdm 6942 | . . . . . . . . . 10
⊢ (𝐴 ∈
(𝑅1‘𝑥) → 𝑥 ∈ dom
𝑅1) | 
| 10 |  | r1sucg 9810 | . . . . . . . . . 10
⊢ (𝑥 ∈ dom
𝑅1 → (𝑅1‘suc 𝑥) = 𝒫
(𝑅1‘𝑥)) | 
| 11 | 9, 10 | syl 17 | . . . . . . . . 9
⊢ (𝐴 ∈
(𝑅1‘𝑥) → (𝑅1‘suc
𝑥) = 𝒫
(𝑅1‘𝑥)) | 
| 12 | 8, 11 | eleqtrrd 2843 | . . . . . . . 8
⊢ (𝐴 ∈
(𝑅1‘𝑥) → 𝐴 ∈ (𝑅1‘suc
𝑥)) | 
| 13 | 12 | a1i 11 | . . . . . . 7
⊢ (𝑥 ∈ On → (𝐴 ∈
(𝑅1‘𝑥) → 𝐴 ∈ (𝑅1‘suc
𝑥))) | 
| 14 | 3, 13 | syl9 77 | . . . . . 6
⊢ (𝐴 ∈ 𝑦 → (𝑥 ∈ On →
((𝑅1‘𝑥) = 𝑦 → 𝐴 ∈ (𝑅1‘suc
𝑥)))) | 
| 15 | 14 | reximdvai 3164 | . . . . 5
⊢ (𝐴 ∈ 𝑦 → (∃𝑥 ∈ On (𝑅1‘𝑥) = 𝑦 → ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘suc
𝑥))) | 
| 16 |  | r1funlim 9807 | . . . . . . 7
⊢ (Fun
𝑅1 ∧ Lim dom 𝑅1) | 
| 17 | 16 | simpli 483 | . . . . . 6
⊢ Fun
𝑅1 | 
| 18 |  | fvelima 6973 | . . . . . 6
⊢ ((Fun
𝑅1 ∧ 𝑦 ∈ (𝑅1 “ On))
→ ∃𝑥 ∈ On
(𝑅1‘𝑥) = 𝑦) | 
| 19 | 17, 18 | mpan 690 | . . . . 5
⊢ (𝑦 ∈ (𝑅1
“ On) → ∃𝑥
∈ On (𝑅1‘𝑥) = 𝑦) | 
| 20 | 15, 19 | impel 505 | . . . 4
⊢ ((𝐴 ∈ 𝑦 ∧ 𝑦 ∈ (𝑅1 “ On))
→ ∃𝑥 ∈ On
𝐴 ∈
(𝑅1‘suc 𝑥)) | 
| 21 | 20 | exlimiv 1929 | . . 3
⊢
(∃𝑦(𝐴 ∈ 𝑦 ∧ 𝑦 ∈ (𝑅1 “ On))
→ ∃𝑥 ∈ On
𝐴 ∈
(𝑅1‘suc 𝑥)) | 
| 22 | 1, 21 | sylbi 217 | . 2
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘suc
𝑥)) | 
| 23 |  | elfvdm 6942 | . . . . . 6
⊢ (𝐴 ∈
(𝑅1‘suc 𝑥) → suc 𝑥 ∈ dom
𝑅1) | 
| 24 |  | fvelrn 7095 | . . . . . 6
⊢ ((Fun
𝑅1 ∧ suc 𝑥 ∈ dom 𝑅1) →
(𝑅1‘suc 𝑥) ∈ ran
𝑅1) | 
| 25 | 17, 23, 24 | sylancr 587 | . . . . 5
⊢ (𝐴 ∈
(𝑅1‘suc 𝑥) → (𝑅1‘suc
𝑥) ∈ ran
𝑅1) | 
| 26 |  | df-ima 5697 | . . . . . 6
⊢
(𝑅1 “ On) = ran (𝑅1 ↾
On) | 
| 27 |  | funrel 6582 | . . . . . . . . 9
⊢ (Fun
𝑅1 → Rel 𝑅1) | 
| 28 | 17, 27 | ax-mp 5 | . . . . . . . 8
⊢ Rel
𝑅1 | 
| 29 | 16 | simpri 485 | . . . . . . . . 9
⊢ Lim dom
𝑅1 | 
| 30 |  | limord 6443 | . . . . . . . . 9
⊢ (Lim dom
𝑅1 → Ord dom 𝑅1) | 
| 31 |  | ordsson 7804 | . . . . . . . . 9
⊢ (Ord dom
𝑅1 → dom 𝑅1 ⊆
On) | 
| 32 | 29, 30, 31 | mp2b 10 | . . . . . . . 8
⊢ dom
𝑅1 ⊆ On | 
| 33 |  | relssres 6039 | . . . . . . . 8
⊢ ((Rel
𝑅1 ∧ dom 𝑅1 ⊆ On) →
(𝑅1 ↾ On) = 𝑅1) | 
| 34 | 28, 32, 33 | mp2an 692 | . . . . . . 7
⊢
(𝑅1 ↾ On) =
𝑅1 | 
| 35 | 34 | rneqi 5947 | . . . . . 6
⊢ ran
(𝑅1 ↾ On) = ran 𝑅1 | 
| 36 | 26, 35 | eqtri 2764 | . . . . 5
⊢
(𝑅1 “ On) = ran
𝑅1 | 
| 37 | 25, 36 | eleqtrrdi 2851 | . . . 4
⊢ (𝐴 ∈
(𝑅1‘suc 𝑥) → (𝑅1‘suc
𝑥) ∈
(𝑅1 “ On)) | 
| 38 |  | elunii 4911 | . . . 4
⊢ ((𝐴 ∈
(𝑅1‘suc 𝑥) ∧ (𝑅1‘suc
𝑥) ∈
(𝑅1 “ On)) → 𝐴 ∈ ∪
(𝑅1 “ On)) | 
| 39 | 37, 38 | mpdan 687 | . . 3
⊢ (𝐴 ∈
(𝑅1‘suc 𝑥) → 𝐴 ∈ ∪
(𝑅1 “ On)) | 
| 40 | 39 | rexlimivw 3150 | . 2
⊢
(∃𝑥 ∈ On
𝐴 ∈
(𝑅1‘suc 𝑥) → 𝐴 ∈ ∪
(𝑅1 “ On)) | 
| 41 | 22, 40 | impbii 209 | 1
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘suc
𝑥)) |