Step | Hyp | Ref
| Expression |
1 | | fveq2 6668 |
. . . 4
⊢ (𝑎 = ∅ → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘∅)) |
2 | | suceq 6231 |
. . . . . 6
⊢ (𝑎 = ∅ → suc 𝑎 = suc ∅) |
3 | 2 | fveq2d 6672 |
. . . . 5
⊢ (𝑎 = ∅ → (rec(𝐺, ∅)‘suc 𝑎) = (rec(𝐺, ∅)‘suc
∅)) |
4 | | fveq2 6668 |
. . . . 5
⊢ (𝑎 = ∅ →
(𝑅1‘𝑎) =
(𝑅1‘∅)) |
5 | 3, 4 | reseq12d 5820 |
. . . 4
⊢ (𝑎 = ∅ → ((rec(𝐺, ∅)‘suc 𝑎) ↾
(𝑅1‘𝑎)) = ((rec(𝐺, ∅)‘suc ∅) ↾
(𝑅1‘∅))) |
6 | 1, 5 | eqeq12d 2754 |
. . 3
⊢ (𝑎 = ∅ → ((rec(𝐺, ∅)‘𝑎) = ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) ↔ (rec(𝐺, ∅)‘∅) = ((rec(𝐺, ∅)‘suc ∅)
↾ (𝑅1‘∅)))) |
7 | | fveq2 6668 |
. . . 4
⊢ (𝑎 = 𝑏 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘𝑏)) |
8 | | suceq 6231 |
. . . . . 6
⊢ (𝑎 = 𝑏 → suc 𝑎 = suc 𝑏) |
9 | 8 | fveq2d 6672 |
. . . . 5
⊢ (𝑎 = 𝑏 → (rec(𝐺, ∅)‘suc 𝑎) = (rec(𝐺, ∅)‘suc 𝑏)) |
10 | | fveq2 6668 |
. . . . 5
⊢ (𝑎 = 𝑏 → (𝑅1‘𝑎) =
(𝑅1‘𝑏)) |
11 | 9, 10 | reseq12d 5820 |
. . . 4
⊢ (𝑎 = 𝑏 → ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) |
12 | 7, 11 | eqeq12d 2754 |
. . 3
⊢ (𝑎 = 𝑏 → ((rec(𝐺, ∅)‘𝑎) = ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) ↔ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))) |
13 | | fveq2 6668 |
. . . 4
⊢ (𝑎 = suc 𝑏 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘suc 𝑏)) |
14 | | suceq 6231 |
. . . . . 6
⊢ (𝑎 = suc 𝑏 → suc 𝑎 = suc suc 𝑏) |
15 | 14 | fveq2d 6672 |
. . . . 5
⊢ (𝑎 = suc 𝑏 → (rec(𝐺, ∅)‘suc 𝑎) = (rec(𝐺, ∅)‘suc suc 𝑏)) |
16 | | fveq2 6668 |
. . . . 5
⊢ (𝑎 = suc 𝑏 → (𝑅1‘𝑎) =
(𝑅1‘suc 𝑏)) |
17 | 15, 16 | reseq12d 5820 |
. . . 4
⊢ (𝑎 = suc 𝑏 → ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) = ((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc
𝑏))) |
18 | 13, 17 | eqeq12d 2754 |
. . 3
⊢ (𝑎 = suc 𝑏 → ((rec(𝐺, ∅)‘𝑎) = ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) ↔ (rec(𝐺, ∅)‘suc 𝑏) = ((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc
𝑏)))) |
19 | | fveq2 6668 |
. . . 4
⊢ (𝑎 = 𝐴 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘𝐴)) |
20 | | suceq 6231 |
. . . . . 6
⊢ (𝑎 = 𝐴 → suc 𝑎 = suc 𝐴) |
21 | 20 | fveq2d 6672 |
. . . . 5
⊢ (𝑎 = 𝐴 → (rec(𝐺, ∅)‘suc 𝑎) = (rec(𝐺, ∅)‘suc 𝐴)) |
22 | | fveq2 6668 |
. . . . 5
⊢ (𝑎 = 𝐴 → (𝑅1‘𝑎) =
(𝑅1‘𝐴)) |
23 | 21, 22 | reseq12d 5820 |
. . . 4
⊢ (𝑎 = 𝐴 → ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) = ((rec(𝐺, ∅)‘suc 𝐴) ↾ (𝑅1‘𝐴))) |
24 | 19, 23 | eqeq12d 2754 |
. . 3
⊢ (𝑎 = 𝐴 → ((rec(𝐺, ∅)‘𝑎) = ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) ↔ (rec(𝐺, ∅)‘𝐴) = ((rec(𝐺, ∅)‘suc 𝐴) ↾ (𝑅1‘𝐴)))) |
25 | | res0 5823 |
. . . 4
⊢
((rec(𝐺,
∅)‘suc ∅) ↾ ∅) = ∅ |
26 | | r10 9263 |
. . . . 5
⊢
(𝑅1‘∅) = ∅ |
27 | 26 | reseq2i 5816 |
. . . 4
⊢
((rec(𝐺,
∅)‘suc ∅) ↾ (𝑅1‘∅)) =
((rec(𝐺, ∅)‘suc
∅) ↾ ∅) |
28 | | 0ex 5172 |
. . . . 5
⊢ ∅
∈ V |
29 | 28 | rdg0 8079 |
. . . 4
⊢
(rec(𝐺,
∅)‘∅) = ∅ |
30 | 25, 27, 29 | 3eqtr4ri 2772 |
. . 3
⊢
(rec(𝐺,
∅)‘∅) = ((rec(𝐺, ∅)‘suc ∅) ↾
(𝑅1‘∅)) |
31 | | peano2 7615 |
. . . . . . . 8
⊢ (𝑏 ∈ ω → suc 𝑏 ∈
ω) |
32 | | ackbij.f |
. . . . . . . . 9
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) |
33 | | ackbij.g |
. . . . . . . . 9
⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦)))) |
34 | 32, 33 | ackbij2lem2 9733 |
. . . . . . . 8
⊢ (suc
𝑏 ∈ ω →
(rec(𝐺, ∅)‘suc
𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc
𝑏))) |
35 | 31, 34 | syl 17 |
. . . . . . 7
⊢ (𝑏 ∈ ω →
(rec(𝐺, ∅)‘suc
𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc
𝑏))) |
36 | | f1ofn 6613 |
. . . . . . 7
⊢
((rec(𝐺,
∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc
𝑏)) → (rec(𝐺, ∅)‘suc 𝑏) Fn
(𝑅1‘suc 𝑏)) |
37 | 35, 36 | syl 17 |
. . . . . 6
⊢ (𝑏 ∈ ω →
(rec(𝐺, ∅)‘suc
𝑏) Fn
(𝑅1‘suc 𝑏)) |
38 | 37 | adantr 484 |
. . . . 5
⊢ ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) → (rec(𝐺, ∅)‘suc 𝑏) Fn
(𝑅1‘suc 𝑏)) |
39 | | peano2 7615 |
. . . . . . . 8
⊢ (suc
𝑏 ∈ ω → suc
suc 𝑏 ∈
ω) |
40 | 32, 33 | ackbij2lem2 9733 |
. . . . . . . 8
⊢ (suc suc
𝑏 ∈ ω →
(rec(𝐺, ∅)‘suc
suc 𝑏):(𝑅1‘suc suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc
suc 𝑏))) |
41 | | f1ofn 6613 |
. . . . . . . 8
⊢
((rec(𝐺,
∅)‘suc suc 𝑏):(𝑅1‘suc suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc
suc 𝑏)) → (rec(𝐺, ∅)‘suc suc 𝑏) Fn
(𝑅1‘suc suc 𝑏)) |
42 | 31, 39, 40, 41 | 4syl 19 |
. . . . . . 7
⊢ (𝑏 ∈ ω →
(rec(𝐺, ∅)‘suc
suc 𝑏) Fn
(𝑅1‘suc suc 𝑏)) |
43 | | nnon 7599 |
. . . . . . . . 9
⊢ (suc
𝑏 ∈ ω → suc
𝑏 ∈
On) |
44 | 31, 43 | syl 17 |
. . . . . . . 8
⊢ (𝑏 ∈ ω → suc 𝑏 ∈ On) |
45 | | r1sssuc 9278 |
. . . . . . . 8
⊢ (suc
𝑏 ∈ On →
(𝑅1‘suc 𝑏) ⊆ (𝑅1‘suc
suc 𝑏)) |
46 | 44, 45 | syl 17 |
. . . . . . 7
⊢ (𝑏 ∈ ω →
(𝑅1‘suc 𝑏) ⊆ (𝑅1‘suc
suc 𝑏)) |
47 | | fnssres 6453 |
. . . . . . 7
⊢
(((rec(𝐺,
∅)‘suc suc 𝑏)
Fn (𝑅1‘suc suc 𝑏) ∧ (𝑅1‘suc
𝑏) ⊆
(𝑅1‘suc suc 𝑏)) → ((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc
𝑏)) Fn
(𝑅1‘suc 𝑏)) |
48 | 42, 46, 47 | syl2anc 587 |
. . . . . 6
⊢ (𝑏 ∈ ω →
((rec(𝐺, ∅)‘suc
suc 𝑏) ↾
(𝑅1‘suc 𝑏)) Fn (𝑅1‘suc 𝑏)) |
49 | 48 | adantr 484 |
. . . . 5
⊢ ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) → ((rec(𝐺, ∅)‘suc suc 𝑏) ↾
(𝑅1‘suc 𝑏)) Fn (𝑅1‘suc 𝑏)) |
50 | | nnon 7599 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ ω → 𝑏 ∈ On) |
51 | | r1suc 9265 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ On →
(𝑅1‘suc 𝑏) = 𝒫
(𝑅1‘𝑏)) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ ω →
(𝑅1‘suc 𝑏) = 𝒫
(𝑅1‘𝑏)) |
53 | 52 | eleq2d 2818 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ ω → (𝑐 ∈
(𝑅1‘suc 𝑏) ↔ 𝑐 ∈ 𝒫
(𝑅1‘𝑏))) |
54 | 53 | biimpa 480 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈
(𝑅1‘suc 𝑏)) → 𝑐 ∈ 𝒫
(𝑅1‘𝑏)) |
55 | 54 | elpwid 4496 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈
(𝑅1‘suc 𝑏)) → 𝑐 ⊆ (𝑅1‘𝑏)) |
56 | | resima2 5854 |
. . . . . . . . . . 11
⊢ (𝑐 ⊆
(𝑅1‘𝑏) → (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐) = ((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐)) |
57 | 55, 56 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈
(𝑅1‘suc 𝑏)) → (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐) = ((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐)) |
58 | 57 | fveq2d 6672 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈
(𝑅1‘suc 𝑏)) → (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐)) = (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐))) |
59 | | fvex 6681 |
. . . . . . . . . . . . 13
⊢
(rec(𝐺,
∅)‘suc 𝑏)
∈ V |
60 | 59 | resex 5867 |
. . . . . . . . . . . 12
⊢
((rec(𝐺,
∅)‘suc 𝑏)
↾ (𝑅1‘𝑏)) ∈ V |
61 | | dmeq 5740 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → dom 𝑥 = dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) |
62 | 61 | pweqd 4504 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → 𝒫 dom 𝑥 = 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾
(𝑅1‘𝑏))) |
63 | | imaeq1 5892 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → (𝑥 “ 𝑦) = (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)) |
64 | 63 | fveq2d 6672 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → (𝐹‘(𝑥 “ 𝑦)) = (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦))) |
65 | 62, 64 | mpteq12dv 5112 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))) = (𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)))) |
66 | 60 | dmex 7635 |
. . . . . . . . . . . . . . 15
⊢ dom
((rec(𝐺, ∅)‘suc
𝑏) ↾
(𝑅1‘𝑏)) ∈ V |
67 | 66 | pwex 5244 |
. . . . . . . . . . . . . 14
⊢ 𝒫
dom ((rec(𝐺,
∅)‘suc 𝑏)
↾ (𝑅1‘𝑏)) ∈ V |
68 | 67 | mptex 6990 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝒫 dom
((rec(𝐺, ∅)‘suc
𝑏) ↾
(𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦))) ∈ V |
69 | 65, 33, 68 | fvmpt 6769 |
. . . . . . . . . . . 12
⊢
(((rec(𝐺,
∅)‘suc 𝑏)
↾ (𝑅1‘𝑏)) ∈ V → (𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) = (𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)))) |
70 | 60, 69 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) = (𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦))) |
71 | 70 | fveq1i 6669 |
. . . . . . . . . 10
⊢ ((𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))‘𝑐) = ((𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)))‘𝑐) |
72 | | r1sssuc 9278 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 ∈ On →
(𝑅1‘𝑏) ⊆ (𝑅1‘suc
𝑏)) |
73 | 50, 72 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 ∈ ω →
(𝑅1‘𝑏) ⊆ (𝑅1‘suc
𝑏)) |
74 | | fnssres 6453 |
. . . . . . . . . . . . . . . 16
⊢
(((rec(𝐺,
∅)‘suc 𝑏) Fn
(𝑅1‘suc 𝑏) ∧ (𝑅1‘𝑏) ⊆
(𝑅1‘suc 𝑏)) → ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) Fn
(𝑅1‘𝑏)) |
75 | 37, 73, 74 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ ω →
((rec(𝐺, ∅)‘suc
𝑏) ↾
(𝑅1‘𝑏)) Fn (𝑅1‘𝑏)) |
76 | 75 | fndmd 6436 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ ω → dom
((rec(𝐺, ∅)‘suc
𝑏) ↾
(𝑅1‘𝑏)) = (𝑅1‘𝑏)) |
77 | 76 | pweqd 4504 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ ω → 𝒫
dom ((rec(𝐺,
∅)‘suc 𝑏)
↾ (𝑅1‘𝑏)) = 𝒫
(𝑅1‘𝑏)) |
78 | 77 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈
(𝑅1‘suc 𝑏)) → 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾
(𝑅1‘𝑏)) = 𝒫
(𝑅1‘𝑏)) |
79 | 54, 78 | eleqtrrd 2836 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈
(𝑅1‘suc 𝑏)) → 𝑐 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) |
80 | | imaeq2 5893 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑐 → (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦) = (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐)) |
81 | 80 | fveq2d 6672 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑐 → (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)) = (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐))) |
82 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝒫 dom
((rec(𝐺, ∅)‘suc
𝑏) ↾
(𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦))) = (𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦))) |
83 | | fvex 6681 |
. . . . . . . . . . . 12
⊢ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐)) ∈ V |
84 | 81, 82, 83 | fvmpt 6769 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ 𝒫 dom
((rec(𝐺, ∅)‘suc
𝑏) ↾
(𝑅1‘𝑏)) → ((𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)))‘𝑐) = (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐))) |
85 | 79, 84 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈
(𝑅1‘suc 𝑏)) → ((𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)))‘𝑐) = (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐))) |
86 | 71, 85 | syl5eq 2785 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈
(𝑅1‘suc 𝑏)) → ((𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))‘𝑐) = (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐))) |
87 | | dmeq 5740 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (rec(𝐺, ∅)‘suc 𝑏) → dom 𝑥 = dom (rec(𝐺, ∅)‘suc 𝑏)) |
88 | 87 | pweqd 4504 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (rec(𝐺, ∅)‘suc 𝑏) → 𝒫 dom 𝑥 = 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏)) |
89 | | imaeq1 5892 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (rec(𝐺, ∅)‘suc 𝑏) → (𝑥 “ 𝑦) = ((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)) |
90 | 89 | fveq2d 6672 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (rec(𝐺, ∅)‘suc 𝑏) → (𝐹‘(𝑥 “ 𝑦)) = (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦))) |
91 | 88, 90 | mpteq12dv 5112 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (rec(𝐺, ∅)‘suc 𝑏) → (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)))) |
92 | 59 | dmex 7635 |
. . . . . . . . . . . . . . 15
⊢ dom
(rec(𝐺, ∅)‘suc
𝑏) ∈
V |
93 | 92 | pwex 5244 |
. . . . . . . . . . . . . 14
⊢ 𝒫
dom (rec(𝐺,
∅)‘suc 𝑏)
∈ V |
94 | 93 | mptex 6990 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦))) ∈ V |
95 | 91, 33, 94 | fvmpt 6769 |
. . . . . . . . . . . 12
⊢
((rec(𝐺,
∅)‘suc 𝑏)
∈ V → (𝐺‘(rec(𝐺, ∅)‘suc 𝑏)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)))) |
96 | 59, 95 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝐺‘(rec(𝐺, ∅)‘suc 𝑏)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦))) |
97 | 96 | fveq1i 6669 |
. . . . . . . . . 10
⊢ ((𝐺‘(rec(𝐺, ∅)‘suc 𝑏))‘𝑐) = ((𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)))‘𝑐) |
98 | | r1tr 9271 |
. . . . . . . . . . . . . . 15
⊢ Tr
(𝑅1‘suc 𝑏) |
99 | 98 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ ω → Tr
(𝑅1‘suc 𝑏)) |
100 | | dftr4 5138 |
. . . . . . . . . . . . . 14
⊢ (Tr
(𝑅1‘suc 𝑏) ↔ (𝑅1‘suc
𝑏) ⊆ 𝒫
(𝑅1‘suc 𝑏)) |
101 | 99, 100 | sylib 221 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ ω →
(𝑅1‘suc 𝑏) ⊆ 𝒫
(𝑅1‘suc 𝑏)) |
102 | 101 | sselda 3875 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈
(𝑅1‘suc 𝑏)) → 𝑐 ∈ 𝒫
(𝑅1‘suc 𝑏)) |
103 | | f1odm 6616 |
. . . . . . . . . . . . . . 15
⊢
((rec(𝐺,
∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc
𝑏)) → dom (rec(𝐺, ∅)‘suc 𝑏) =
(𝑅1‘suc 𝑏)) |
104 | 35, 103 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ ω → dom
(rec(𝐺, ∅)‘suc
𝑏) =
(𝑅1‘suc 𝑏)) |
105 | 104 | pweqd 4504 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ ω → 𝒫
dom (rec(𝐺,
∅)‘suc 𝑏) =
𝒫 (𝑅1‘suc 𝑏)) |
106 | 105 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈
(𝑅1‘suc 𝑏)) → 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) = 𝒫
(𝑅1‘suc 𝑏)) |
107 | 102, 106 | eleqtrrd 2836 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈
(𝑅1‘suc 𝑏)) → 𝑐 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏)) |
108 | | imaeq2 5893 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑐 → ((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦) = ((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐)) |
109 | 108 | fveq2d 6672 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑐 → (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)) = (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐))) |
110 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦))) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦))) |
111 | | fvex 6681 |
. . . . . . . . . . . 12
⊢ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐)) ∈ V |
112 | 109, 110,
111 | fvmpt 6769 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) → ((𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)))‘𝑐) = (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐))) |
113 | 107, 112 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈
(𝑅1‘suc 𝑏)) → ((𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)))‘𝑐) = (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐))) |
114 | 97, 113 | syl5eq 2785 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈
(𝑅1‘suc 𝑏)) → ((𝐺‘(rec(𝐺, ∅)‘suc 𝑏))‘𝑐) = (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐))) |
115 | 58, 86, 114 | 3eqtr4d 2783 |
. . . . . . . 8
⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈
(𝑅1‘suc 𝑏)) → ((𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘suc 𝑏))‘𝑐)) |
116 | 115 | adantlr 715 |
. . . . . . 7
⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc
𝑏)) → ((𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘suc 𝑏))‘𝑐)) |
117 | | fveq2 6668 |
. . . . . . . . 9
⊢
((rec(𝐺,
∅)‘𝑏) =
((rec(𝐺, ∅)‘suc
𝑏) ↾
(𝑅1‘𝑏)) → (𝐺‘(rec(𝐺, ∅)‘𝑏)) = (𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))) |
118 | 117 | fveq1d 6670 |
. . . . . . . 8
⊢
((rec(𝐺,
∅)‘𝑏) =
((rec(𝐺, ∅)‘suc
𝑏) ↾
(𝑅1‘𝑏)) → ((𝐺‘(rec(𝐺, ∅)‘𝑏))‘𝑐) = ((𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))‘𝑐)) |
119 | 118 | ad2antlr 727 |
. . . . . . 7
⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc
𝑏)) → ((𝐺‘(rec(𝐺, ∅)‘𝑏))‘𝑐) = ((𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))‘𝑐)) |
120 | | rdgsuc 8082 |
. . . . . . . . . 10
⊢ (suc
𝑏 ∈ On →
(rec(𝐺, ∅)‘suc
suc 𝑏) = (𝐺‘(rec(𝐺, ∅)‘suc 𝑏))) |
121 | 44, 120 | syl 17 |
. . . . . . . . 9
⊢ (𝑏 ∈ ω →
(rec(𝐺, ∅)‘suc
suc 𝑏) = (𝐺‘(rec(𝐺, ∅)‘suc 𝑏))) |
122 | 121 | fveq1d 6670 |
. . . . . . . 8
⊢ (𝑏 ∈ ω →
((rec(𝐺, ∅)‘suc
suc 𝑏)‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘suc 𝑏))‘𝑐)) |
123 | 122 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc
𝑏)) → ((rec(𝐺, ∅)‘suc suc 𝑏)‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘suc 𝑏))‘𝑐)) |
124 | 116, 119,
123 | 3eqtr4rd 2784 |
. . . . . 6
⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc
𝑏)) → ((rec(𝐺, ∅)‘suc suc 𝑏)‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘𝑏))‘𝑐)) |
125 | | fvres 6687 |
. . . . . . 7
⊢ (𝑐 ∈
(𝑅1‘suc 𝑏) → (((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc
𝑏))‘𝑐) = ((rec(𝐺, ∅)‘suc suc 𝑏)‘𝑐)) |
126 | 125 | adantl 485 |
. . . . . 6
⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc
𝑏)) → (((rec(𝐺, ∅)‘suc suc 𝑏) ↾
(𝑅1‘suc 𝑏))‘𝑐) = ((rec(𝐺, ∅)‘suc suc 𝑏)‘𝑐)) |
127 | | rdgsuc 8082 |
. . . . . . . . 9
⊢ (𝑏 ∈ On → (rec(𝐺, ∅)‘suc 𝑏) = (𝐺‘(rec(𝐺, ∅)‘𝑏))) |
128 | 50, 127 | syl 17 |
. . . . . . . 8
⊢ (𝑏 ∈ ω →
(rec(𝐺, ∅)‘suc
𝑏) = (𝐺‘(rec(𝐺, ∅)‘𝑏))) |
129 | 128 | fveq1d 6670 |
. . . . . . 7
⊢ (𝑏 ∈ ω →
((rec(𝐺, ∅)‘suc
𝑏)‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘𝑏))‘𝑐)) |
130 | 129 | ad2antrr 726 |
. . . . . 6
⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc
𝑏)) → ((rec(𝐺, ∅)‘suc 𝑏)‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘𝑏))‘𝑐)) |
131 | 124, 126,
130 | 3eqtr4rd 2784 |
. . . . 5
⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc
𝑏)) → ((rec(𝐺, ∅)‘suc 𝑏)‘𝑐) = (((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc
𝑏))‘𝑐)) |
132 | 38, 49, 131 | eqfnfvd 6806 |
. . . 4
⊢ ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) → (rec(𝐺, ∅)‘suc 𝑏) = ((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc
𝑏))) |
133 | 132 | ex 416 |
. . 3
⊢ (𝑏 ∈ ω →
((rec(𝐺,
∅)‘𝑏) =
((rec(𝐺, ∅)‘suc
𝑏) ↾
(𝑅1‘𝑏)) → (rec(𝐺, ∅)‘suc 𝑏) = ((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc
𝑏)))) |
134 | 6, 12, 18, 24, 30, 133 | finds 7622 |
. 2
⊢ (𝐴 ∈ ω →
(rec(𝐺,
∅)‘𝐴) =
((rec(𝐺, ∅)‘suc
𝐴) ↾
(𝑅1‘𝐴))) |
135 | | resss 5844 |
. 2
⊢
((rec(𝐺,
∅)‘suc 𝐴)
↾ (𝑅1‘𝐴)) ⊆ (rec(𝐺, ∅)‘suc 𝐴) |
136 | 134, 135 | eqsstrdi 3929 |
1
⊢ (𝐴 ∈ ω →
(rec(𝐺,
∅)‘𝐴) ⊆
(rec(𝐺, ∅)‘suc
𝐴)) |