Step | Hyp | Ref
| Expression |
1 | | df-ttrcl 33530 |
. . . . 5
⊢ t++𝑅 = {〈𝑥, 𝑦〉 ∣ ∃𝑛 ∈ (ω ∖
1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))} |
2 | 1 | rneqi 5821 |
. . . 4
⊢ ran
t++𝑅 = ran {〈𝑥, 𝑦〉 ∣ ∃𝑛 ∈ (ω ∖
1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))} |
3 | | rnopab 5838 |
. . . 4
⊢ ran
{〈𝑥, 𝑦〉 ∣ ∃𝑛 ∈ (ω ∖
1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))} = {𝑦 ∣ ∃𝑥∃𝑛 ∈ (ω ∖
1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))} |
4 | 2, 3 | eqtri 2766 |
. . 3
⊢ ran
t++𝑅 = {𝑦 ∣ ∃𝑥∃𝑛 ∈ (ω ∖
1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))} |
5 | | fveq2 6736 |
. . . . . . . . . . . 12
⊢ (𝑎 = ∪
𝑛 → (𝑓‘𝑎) = (𝑓‘∪ 𝑛)) |
6 | | suceq 6296 |
. . . . . . . . . . . . 13
⊢ (𝑎 = ∪
𝑛 → suc 𝑎 = suc ∪ 𝑛) |
7 | 6 | fveq2d 6740 |
. . . . . . . . . . . 12
⊢ (𝑎 = ∪
𝑛 → (𝑓‘suc 𝑎) = (𝑓‘suc ∪ 𝑛)) |
8 | 5, 7 | breq12d 5081 |
. . . . . . . . . . 11
⊢ (𝑎 = ∪
𝑛 → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘∪ 𝑛)𝑅(𝑓‘suc ∪ 𝑛))) |
9 | | simpr3 1198 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ (𝑓 Fn
suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) |
10 | | df-1o 8223 |
. . . . . . . . . . . . . . . 16
⊢
1o = suc ∅ |
11 | 10 | difeq2i 4049 |
. . . . . . . . . . . . . . 15
⊢ (ω
∖ 1o) = (ω ∖ suc ∅) |
12 | 11 | eleq2i 2830 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (ω ∖
1o) ↔ 𝑛
∈ (ω ∖ suc ∅)) |
13 | | peano1 7686 |
. . . . . . . . . . . . . . 15
⊢ ∅
∈ ω |
14 | | eldifsucnn 33433 |
. . . . . . . . . . . . . . 15
⊢ (∅
∈ ω → (𝑛
∈ (ω ∖ suc ∅) ↔ ∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥)) |
15 | 13, 14 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (ω ∖ suc
∅) ↔ ∃𝑥
∈ (ω ∖ ∅)𝑛 = suc 𝑥) |
16 | | dif0 4302 |
. . . . . . . . . . . . . . 15
⊢ (ω
∖ ∅) = ω |
17 | 16 | rexeqi 3337 |
. . . . . . . . . . . . . 14
⊢
(∃𝑥 ∈
(ω ∖ ∅)𝑛
= suc 𝑥 ↔ ∃𝑥 ∈ ω 𝑛 = suc 𝑥) |
18 | 12, 15, 17 | 3bitri 300 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (ω ∖
1o) ↔ ∃𝑥 ∈ ω 𝑛 = suc 𝑥) |
19 | | nnord 7671 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ω → Ord 𝑥) |
20 | | ordunisuc 7630 |
. . . . . . . . . . . . . . . . 17
⊢ (Ord
𝑥 → ∪ suc 𝑥 = 𝑥) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ω → ∪ suc 𝑥 = 𝑥) |
22 | | vex 3425 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑥 ∈ V |
23 | 22 | sucid 6310 |
. . . . . . . . . . . . . . . 16
⊢ 𝑥 ∈ suc 𝑥 |
24 | 21, 23 | eqeltrdi 2847 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ω → ∪ suc 𝑥 ∈ suc 𝑥) |
25 | | unieq 4845 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = suc 𝑥 → ∪ 𝑛 = ∪
suc 𝑥) |
26 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = suc 𝑥 → 𝑛 = suc 𝑥) |
27 | 25, 26 | eleq12d 2833 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = suc 𝑥 → (∪ 𝑛 ∈ 𝑛 ↔ ∪ suc
𝑥 ∈ suc 𝑥)) |
28 | 24, 27 | syl5ibrcom 250 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ω → (𝑛 = suc 𝑥 → ∪ 𝑛 ∈ 𝑛)) |
29 | 28 | rexlimiv 3207 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
ω 𝑛 = suc 𝑥 → ∪ 𝑛
∈ 𝑛) |
30 | 18, 29 | sylbi 220 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (ω ∖
1o) → ∪ 𝑛 ∈ 𝑛) |
31 | 30 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ (𝑓 Fn
suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∪ 𝑛 ∈ 𝑛) |
32 | 8, 9, 31 | rspcdva 3552 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ (𝑓 Fn
suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘∪ 𝑛)𝑅(𝑓‘suc ∪ 𝑛)) |
33 | | suceq 6296 |
. . . . . . . . . . . . . . . . 17
⊢ (∪ suc 𝑥 = 𝑥 → suc ∪ suc
𝑥 = suc 𝑥) |
34 | 21, 33 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ω → suc ∪ suc 𝑥 = suc 𝑥) |
35 | | suceq 6296 |
. . . . . . . . . . . . . . . . . 18
⊢ (∪ 𝑛 =
∪ suc 𝑥 → suc ∪
𝑛 = suc ∪ suc 𝑥) |
36 | 25, 35 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = suc 𝑥 → suc ∪
𝑛 = suc ∪ suc 𝑥) |
37 | 36, 26 | eqeq12d 2754 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = suc 𝑥 → (suc ∪
𝑛 = 𝑛 ↔ suc ∪ suc
𝑥 = suc 𝑥)) |
38 | 34, 37 | syl5ibrcom 250 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ω → (𝑛 = suc 𝑥 → suc ∪
𝑛 = 𝑛)) |
39 | 38 | rexlimiv 3207 |
. . . . . . . . . . . . . 14
⊢
(∃𝑥 ∈
ω 𝑛 = suc 𝑥 → suc ∪ 𝑛 =
𝑛) |
40 | 18, 39 | sylbi 220 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (ω ∖
1o) → suc ∪ 𝑛 = 𝑛) |
41 | 40 | fveq2d 6740 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (ω ∖
1o) → (𝑓‘suc ∪ 𝑛) = (𝑓‘𝑛)) |
42 | 41 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ (𝑓 Fn
suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘suc ∪ 𝑛) = (𝑓‘𝑛)) |
43 | | simpr2r 1235 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ (𝑓 Fn
suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘𝑛) = 𝑦) |
44 | 42, 43 | eqtrd 2778 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ (𝑓 Fn
suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘suc ∪ 𝑛) = 𝑦) |
45 | 32, 44 | breqtrd 5094 |
. . . . . . . . 9
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ (𝑓 Fn
suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘∪ 𝑛)𝑅𝑦) |
46 | | fvex 6749 |
. . . . . . . . . 10
⊢ (𝑓‘∪ 𝑛)
∈ V |
47 | | vex 3425 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
48 | 46, 47 | brelrn 5826 |
. . . . . . . . 9
⊢ ((𝑓‘∪ 𝑛)𝑅𝑦 → 𝑦 ∈ ran 𝑅) |
49 | 45, 48 | syl 17 |
. . . . . . . 8
⊢ ((𝑛 ∈ (ω ∖
1o) ∧ (𝑓 Fn
suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → 𝑦 ∈ ran 𝑅) |
50 | 49 | ex 416 |
. . . . . . 7
⊢ (𝑛 ∈ (ω ∖
1o) → ((𝑓
Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑦 ∈ ran 𝑅)) |
51 | 50 | exlimdv 1941 |
. . . . . 6
⊢ (𝑛 ∈ (ω ∖
1o) → (∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑦 ∈ ran 𝑅)) |
52 | 51 | rexlimiv 3207 |
. . . . 5
⊢
(∃𝑛 ∈
(ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑦 ∈ ran 𝑅) |
53 | 52 | exlimiv 1938 |
. . . 4
⊢
(∃𝑥∃𝑛 ∈ (ω ∖
1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑦 ∈ ran 𝑅) |
54 | 53 | abssi 3998 |
. . 3
⊢ {𝑦 ∣ ∃𝑥∃𝑛 ∈ (ω ∖
1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))} ⊆ ran 𝑅 |
55 | 4, 54 | eqsstri 3950 |
. 2
⊢ ran
t++𝑅 ⊆ ran 𝑅 |
56 | | rnresv 6079 |
. . 3
⊢ ran
(𝑅 ↾ V) = ran 𝑅 |
57 | | relres 5895 |
. . . . . 6
⊢ Rel
(𝑅 ↾
V) |
58 | | ssttrcl 33537 |
. . . . . 6
⊢ (Rel
(𝑅 ↾ V) → (𝑅 ↾ V) ⊆ t++(𝑅 ↾ V)) |
59 | 57, 58 | ax-mp 5 |
. . . . 5
⊢ (𝑅 ↾ V) ⊆ t++(𝑅 ↾ V) |
60 | | ttrclresv 33539 |
. . . . 5
⊢ t++(𝑅 ↾ V) = t++𝑅 |
61 | 59, 60 | sseqtri 3952 |
. . . 4
⊢ (𝑅 ↾ V) ⊆ t++𝑅 |
62 | 61 | rnssi 5824 |
. . 3
⊢ ran
(𝑅 ↾ V) ⊆ ran
t++𝑅 |
63 | 56, 62 | eqsstrri 3951 |
. 2
⊢ ran 𝑅 ⊆ ran t++𝑅 |
64 | 55, 63 | eqssi 3932 |
1
⊢ ran
t++𝑅 = ran 𝑅 |