| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-ttrcl 9749 | . . . . 5
⊢ t++𝑅 = {〈𝑥, 𝑦〉 ∣ ∃𝑛 ∈ (ω ∖
1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))} | 
| 2 | 1 | rneqi 5947 | . . . 4
⊢ ran
t++𝑅 = ran {〈𝑥, 𝑦〉 ∣ ∃𝑛 ∈ (ω ∖
1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))} | 
| 3 |  | rnopab 5964 | . . . 4
⊢ ran
{〈𝑥, 𝑦〉 ∣ ∃𝑛 ∈ (ω ∖
1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))} = {𝑦 ∣ ∃𝑥∃𝑛 ∈ (ω ∖
1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))} | 
| 4 | 2, 3 | eqtri 2764 | . . 3
⊢ ran
t++𝑅 = {𝑦 ∣ ∃𝑥∃𝑛 ∈ (ω ∖
1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))} | 
| 5 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑎 = ∪
𝑛 → (𝑓‘𝑎) = (𝑓‘∪ 𝑛)) | 
| 6 |  | suceq 6449 | . . . . . . . . . . . . 13
⊢ (𝑎 = ∪
𝑛 → suc 𝑎 = suc ∪ 𝑛) | 
| 7 | 6 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (𝑎 = ∪
𝑛 → (𝑓‘suc 𝑎) = (𝑓‘suc ∪ 𝑛)) | 
| 8 | 5, 7 | breq12d 5155 | . . . . . . . . . . 11
⊢ (𝑎 = ∪
𝑛 → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘∪ 𝑛)𝑅(𝑓‘suc ∪ 𝑛))) | 
| 9 |  | simpr3 1196 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ (𝑓 Fn
suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) | 
| 10 |  | df-1o 8507 | . . . . . . . . . . . . . . . 16
⊢
1o = suc ∅ | 
| 11 | 10 | difeq2i 4122 | . . . . . . . . . . . . . . 15
⊢ (ω
∖ 1o) = (ω ∖ suc ∅) | 
| 12 | 11 | eleq2i 2832 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (ω ∖
1o) ↔ 𝑛
∈ (ω ∖ suc ∅)) | 
| 13 |  | peano1 7911 | . . . . . . . . . . . . . . 15
⊢ ∅
∈ ω | 
| 14 |  | eldifsucnn 8703 | . . . . . . . . . . . . . . 15
⊢ (∅
∈ ω → (𝑛
∈ (ω ∖ suc ∅) ↔ ∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥)) | 
| 15 | 13, 14 | ax-mp 5 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (ω ∖ suc
∅) ↔ ∃𝑥
∈ (ω ∖ ∅)𝑛 = suc 𝑥) | 
| 16 |  | dif0 4377 | . . . . . . . . . . . . . . 15
⊢ (ω
∖ ∅) = ω | 
| 17 | 16 | rexeqi 3324 | . . . . . . . . . . . . . 14
⊢
(∃𝑥 ∈
(ω ∖ ∅)𝑛
= suc 𝑥 ↔ ∃𝑥 ∈ ω 𝑛 = suc 𝑥) | 
| 18 | 12, 15, 17 | 3bitri 297 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ (ω ∖
1o) ↔ ∃𝑥 ∈ ω 𝑛 = suc 𝑥) | 
| 19 |  | nnord 7896 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ω → Ord 𝑥) | 
| 20 |  | ordunisuc 7853 | . . . . . . . . . . . . . . . . 17
⊢ (Ord
𝑥 → ∪ suc 𝑥 = 𝑥) | 
| 21 | 19, 20 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ω → ∪ suc 𝑥 = 𝑥) | 
| 22 |  | vex 3483 | . . . . . . . . . . . . . . . . 17
⊢ 𝑥 ∈ V | 
| 23 | 22 | sucid 6465 | . . . . . . . . . . . . . . . 16
⊢ 𝑥 ∈ suc 𝑥 | 
| 24 | 21, 23 | eqeltrdi 2848 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ω → ∪ suc 𝑥 ∈ suc 𝑥) | 
| 25 |  | unieq 4917 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 = suc 𝑥 → ∪ 𝑛 = ∪
suc 𝑥) | 
| 26 |  | id 22 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 = suc 𝑥 → 𝑛 = suc 𝑥) | 
| 27 | 25, 26 | eleq12d 2834 | . . . . . . . . . . . . . . 15
⊢ (𝑛 = suc 𝑥 → (∪ 𝑛 ∈ 𝑛 ↔ ∪ suc
𝑥 ∈ suc 𝑥)) | 
| 28 | 24, 27 | syl5ibrcom 247 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ω → (𝑛 = suc 𝑥 → ∪ 𝑛 ∈ 𝑛)) | 
| 29 | 28 | rexlimiv 3147 | . . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
ω 𝑛 = suc 𝑥 → ∪ 𝑛
∈ 𝑛) | 
| 30 | 18, 29 | sylbi 217 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ (ω ∖
1o) → ∪ 𝑛 ∈ 𝑛) | 
| 31 | 30 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ (𝑓 Fn
suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∪ 𝑛 ∈ 𝑛) | 
| 32 | 8, 9, 31 | rspcdva 3622 | . . . . . . . . . 10
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ (𝑓 Fn
suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘∪ 𝑛)𝑅(𝑓‘suc ∪ 𝑛)) | 
| 33 |  | suceq 6449 | . . . . . . . . . . . . . . . . 17
⊢ (∪ suc 𝑥 = 𝑥 → suc ∪ suc
𝑥 = suc 𝑥) | 
| 34 | 21, 33 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ω → suc ∪ suc 𝑥 = suc 𝑥) | 
| 35 |  | suceq 6449 | . . . . . . . . . . . . . . . . . 18
⊢ (∪ 𝑛 =
∪ suc 𝑥 → suc ∪
𝑛 = suc ∪ suc 𝑥) | 
| 36 | 25, 35 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 = suc 𝑥 → suc ∪
𝑛 = suc ∪ suc 𝑥) | 
| 37 | 36, 26 | eqeq12d 2752 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 = suc 𝑥 → (suc ∪
𝑛 = 𝑛 ↔ suc ∪ suc
𝑥 = suc 𝑥)) | 
| 38 | 34, 37 | syl5ibrcom 247 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ω → (𝑛 = suc 𝑥 → suc ∪
𝑛 = 𝑛)) | 
| 39 | 38 | rexlimiv 3147 | . . . . . . . . . . . . . 14
⊢
(∃𝑥 ∈
ω 𝑛 = suc 𝑥 → suc ∪ 𝑛 =
𝑛) | 
| 40 | 18, 39 | sylbi 217 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ (ω ∖
1o) → suc ∪ 𝑛 = 𝑛) | 
| 41 | 40 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ (ω ∖
1o) → (𝑓‘suc ∪ 𝑛) = (𝑓‘𝑛)) | 
| 42 | 41 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ (𝑓 Fn
suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘suc ∪ 𝑛) = (𝑓‘𝑛)) | 
| 43 |  | simpr2r 1233 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ (𝑓 Fn
suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘𝑛) = 𝑦) | 
| 44 | 42, 43 | eqtrd 2776 | . . . . . . . . . 10
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ (𝑓 Fn
suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘suc ∪ 𝑛) = 𝑦) | 
| 45 | 32, 44 | breqtrd 5168 | . . . . . . . . 9
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ (𝑓 Fn
suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘∪ 𝑛)𝑅𝑦) | 
| 46 |  | fvex 6918 | . . . . . . . . . 10
⊢ (𝑓‘∪ 𝑛)
∈ V | 
| 47 |  | vex 3483 | . . . . . . . . . 10
⊢ 𝑦 ∈ V | 
| 48 | 46, 47 | brelrn 5952 | . . . . . . . . 9
⊢ ((𝑓‘∪ 𝑛)𝑅𝑦 → 𝑦 ∈ ran 𝑅) | 
| 49 | 45, 48 | syl 17 | . . . . . . . 8
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ (𝑓 Fn
suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → 𝑦 ∈ ran 𝑅) | 
| 50 | 49 | ex 412 | . . . . . . 7
⊢ (𝑛 ∈ (ω ∖
1o) → ((𝑓
Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑦 ∈ ran 𝑅)) | 
| 51 | 50 | exlimdv 1932 | . . . . . 6
⊢ (𝑛 ∈ (ω ∖
1o) → (∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑦 ∈ ran 𝑅)) | 
| 52 | 51 | rexlimiv 3147 | . . . . 5
⊢
(∃𝑛 ∈
(ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑦 ∈ ran 𝑅) | 
| 53 | 52 | exlimiv 1929 | . . . 4
⊢
(∃𝑥∃𝑛 ∈ (ω ∖
1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑦 ∈ ran 𝑅) | 
| 54 | 53 | abssi 4069 | . . 3
⊢ {𝑦 ∣ ∃𝑥∃𝑛 ∈ (ω ∖
1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))} ⊆ ran 𝑅 | 
| 55 | 4, 54 | eqsstri 4029 | . 2
⊢ ran
t++𝑅 ⊆ ran 𝑅 | 
| 56 |  | rnresv 6220 | . . 3
⊢ ran
(𝑅 ↾ V) = ran 𝑅 | 
| 57 |  | relres 6022 | . . . . . 6
⊢ Rel
(𝑅 ↾
V) | 
| 58 |  | ssttrcl 9756 | . . . . . 6
⊢ (Rel
(𝑅 ↾ V) → (𝑅 ↾ V) ⊆ t++(𝑅 ↾ V)) | 
| 59 | 57, 58 | ax-mp 5 | . . . . 5
⊢ (𝑅 ↾ V) ⊆ t++(𝑅 ↾ V) | 
| 60 |  | ttrclresv 9758 | . . . . 5
⊢ t++(𝑅 ↾ V) = t++𝑅 | 
| 61 | 59, 60 | sseqtri 4031 | . . . 4
⊢ (𝑅 ↾ V) ⊆ t++𝑅 | 
| 62 | 61 | rnssi 5950 | . . 3
⊢ ran
(𝑅 ↾ V) ⊆ ran
t++𝑅 | 
| 63 | 56, 62 | eqsstrri 4030 | . 2
⊢ ran 𝑅 ⊆ ran t++𝑅 | 
| 64 | 55, 63 | eqssi 3999 | 1
⊢ ran
t++𝑅 = ran 𝑅 |