Step |
Hyp |
Ref |
Expression |
1 |
|
ackbij.f |
⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) ) |
2 |
|
ackbij.g |
⊢ 𝐺 = ( 𝑥 ∈ V ↦ ( 𝑦 ∈ 𝒫 dom 𝑥 ↦ ( 𝐹 ‘ ( 𝑥 “ 𝑦 ) ) ) ) |
3 |
|
fveq2 |
⊢ ( 𝑎 = ∅ → ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) = ( rec ( 𝐺 , ∅ ) ‘ ∅ ) ) |
4 |
|
suceq |
⊢ ( 𝑎 = ∅ → suc 𝑎 = suc ∅ ) |
5 |
4
|
fveq2d |
⊢ ( 𝑎 = ∅ → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑎 ) = ( rec ( 𝐺 , ∅ ) ‘ suc ∅ ) ) |
6 |
|
fveq2 |
⊢ ( 𝑎 = ∅ → ( 𝑅1 ‘ 𝑎 ) = ( 𝑅1 ‘ ∅ ) ) |
7 |
5 6
|
reseq12d |
⊢ ( 𝑎 = ∅ → ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑎 ) ↾ ( 𝑅1 ‘ 𝑎 ) ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc ∅ ) ↾ ( 𝑅1 ‘ ∅ ) ) ) |
8 |
3 7
|
eqeq12d |
⊢ ( 𝑎 = ∅ → ( ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑎 ) ↾ ( 𝑅1 ‘ 𝑎 ) ) ↔ ( rec ( 𝐺 , ∅ ) ‘ ∅ ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc ∅ ) ↾ ( 𝑅1 ‘ ∅ ) ) ) ) |
9 |
|
fveq2 |
⊢ ( 𝑎 = 𝑏 → ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) = ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) |
10 |
|
suceq |
⊢ ( 𝑎 = 𝑏 → suc 𝑎 = suc 𝑏 ) |
11 |
10
|
fveq2d |
⊢ ( 𝑎 = 𝑏 → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑎 ) = ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) |
12 |
|
fveq2 |
⊢ ( 𝑎 = 𝑏 → ( 𝑅1 ‘ 𝑎 ) = ( 𝑅1 ‘ 𝑏 ) ) |
13 |
11 12
|
reseq12d |
⊢ ( 𝑎 = 𝑏 → ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑎 ) ↾ ( 𝑅1 ‘ 𝑎 ) ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) |
14 |
9 13
|
eqeq12d |
⊢ ( 𝑎 = 𝑏 → ( ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑎 ) ↾ ( 𝑅1 ‘ 𝑎 ) ) ↔ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) ) |
15 |
|
fveq2 |
⊢ ( 𝑎 = suc 𝑏 → ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) = ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) |
16 |
|
suceq |
⊢ ( 𝑎 = suc 𝑏 → suc 𝑎 = suc suc 𝑏 ) |
17 |
16
|
fveq2d |
⊢ ( 𝑎 = suc 𝑏 → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑎 ) = ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ) |
18 |
|
fveq2 |
⊢ ( 𝑎 = suc 𝑏 → ( 𝑅1 ‘ 𝑎 ) = ( 𝑅1 ‘ suc 𝑏 ) ) |
19 |
17 18
|
reseq12d |
⊢ ( 𝑎 = suc 𝑏 → ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑎 ) ↾ ( 𝑅1 ‘ 𝑎 ) ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ↾ ( 𝑅1 ‘ suc 𝑏 ) ) ) |
20 |
15 19
|
eqeq12d |
⊢ ( 𝑎 = suc 𝑏 → ( ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑎 ) ↾ ( 𝑅1 ‘ 𝑎 ) ) ↔ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ↾ ( 𝑅1 ‘ suc 𝑏 ) ) ) ) |
21 |
|
fveq2 |
⊢ ( 𝑎 = 𝐴 → ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) = ( rec ( 𝐺 , ∅ ) ‘ 𝐴 ) ) |
22 |
|
suceq |
⊢ ( 𝑎 = 𝐴 → suc 𝑎 = suc 𝐴 ) |
23 |
22
|
fveq2d |
⊢ ( 𝑎 = 𝐴 → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑎 ) = ( rec ( 𝐺 , ∅ ) ‘ suc 𝐴 ) ) |
24 |
|
fveq2 |
⊢ ( 𝑎 = 𝐴 → ( 𝑅1 ‘ 𝑎 ) = ( 𝑅1 ‘ 𝐴 ) ) |
25 |
23 24
|
reseq12d |
⊢ ( 𝑎 = 𝐴 → ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑎 ) ↾ ( 𝑅1 ‘ 𝑎 ) ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝐴 ) ↾ ( 𝑅1 ‘ 𝐴 ) ) ) |
26 |
21 25
|
eqeq12d |
⊢ ( 𝑎 = 𝐴 → ( ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑎 ) ↾ ( 𝑅1 ‘ 𝑎 ) ) ↔ ( rec ( 𝐺 , ∅ ) ‘ 𝐴 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝐴 ) ↾ ( 𝑅1 ‘ 𝐴 ) ) ) ) |
27 |
|
res0 |
⊢ ( ( rec ( 𝐺 , ∅ ) ‘ suc ∅ ) ↾ ∅ ) = ∅ |
28 |
|
r10 |
⊢ ( 𝑅1 ‘ ∅ ) = ∅ |
29 |
28
|
reseq2i |
⊢ ( ( rec ( 𝐺 , ∅ ) ‘ suc ∅ ) ↾ ( 𝑅1 ‘ ∅ ) ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc ∅ ) ↾ ∅ ) |
30 |
|
0ex |
⊢ ∅ ∈ V |
31 |
30
|
rdg0 |
⊢ ( rec ( 𝐺 , ∅ ) ‘ ∅ ) = ∅ |
32 |
27 29 31
|
3eqtr4ri |
⊢ ( rec ( 𝐺 , ∅ ) ‘ ∅ ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc ∅ ) ↾ ( 𝑅1 ‘ ∅ ) ) |
33 |
|
peano2 |
⊢ ( 𝑏 ∈ ω → suc 𝑏 ∈ ω ) |
34 |
1 2
|
ackbij2lem2 |
⊢ ( suc 𝑏 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) : ( 𝑅1 ‘ suc 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) ) |
35 |
33 34
|
syl |
⊢ ( 𝑏 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) : ( 𝑅1 ‘ suc 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) ) |
36 |
|
f1ofn |
⊢ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) : ( 𝑅1 ‘ suc 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) Fn ( 𝑅1 ‘ suc 𝑏 ) ) |
37 |
35 36
|
syl |
⊢ ( 𝑏 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) Fn ( 𝑅1 ‘ suc 𝑏 ) ) |
38 |
37
|
adantr |
⊢ ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) Fn ( 𝑅1 ‘ suc 𝑏 ) ) |
39 |
|
peano2 |
⊢ ( suc 𝑏 ∈ ω → suc suc 𝑏 ∈ ω ) |
40 |
1 2
|
ackbij2lem2 |
⊢ ( suc suc 𝑏 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) : ( 𝑅1 ‘ suc suc 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ suc suc 𝑏 ) ) ) |
41 |
|
f1ofn |
⊢ ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) : ( 𝑅1 ‘ suc suc 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ suc suc 𝑏 ) ) → ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) Fn ( 𝑅1 ‘ suc suc 𝑏 ) ) |
42 |
33 39 40 41
|
4syl |
⊢ ( 𝑏 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) Fn ( 𝑅1 ‘ suc suc 𝑏 ) ) |
43 |
|
nnon |
⊢ ( suc 𝑏 ∈ ω → suc 𝑏 ∈ On ) |
44 |
33 43
|
syl |
⊢ ( 𝑏 ∈ ω → suc 𝑏 ∈ On ) |
45 |
|
r1sssuc |
⊢ ( suc 𝑏 ∈ On → ( 𝑅1 ‘ suc 𝑏 ) ⊆ ( 𝑅1 ‘ suc suc 𝑏 ) ) |
46 |
44 45
|
syl |
⊢ ( 𝑏 ∈ ω → ( 𝑅1 ‘ suc 𝑏 ) ⊆ ( 𝑅1 ‘ suc suc 𝑏 ) ) |
47 |
|
fnssres |
⊢ ( ( ( 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 |
⊢ ( 𝑏 ∈ ω → ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ↾ ( 𝑅1 ‘ suc 𝑏 ) ) Fn ( 𝑅1 ‘ suc 𝑏 ) ) |
49 |
48
|
adantr |
⊢ ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) → ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ↾ ( 𝑅1 ‘ suc 𝑏 ) ) Fn ( 𝑅1 ‘ suc 𝑏 ) ) |
50 |
|
nnon |
⊢ ( 𝑏 ∈ ω → 𝑏 ∈ On ) |
51 |
|
r1suc |
⊢ ( 𝑏 ∈ On → ( 𝑅1 ‘ suc 𝑏 ) = 𝒫 ( 𝑅1 ‘ 𝑏 ) ) |
52 |
50 51
|
syl |
⊢ ( 𝑏 ∈ ω → ( 𝑅1 ‘ suc 𝑏 ) = 𝒫 ( 𝑅1 ‘ 𝑏 ) ) |
53 |
52
|
eleq2d |
⊢ ( 𝑏 ∈ ω → ( 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ↔ 𝑐 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ) ) |
54 |
53
|
biimpa |
⊢ ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → 𝑐 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ) |
55 |
54
|
elpwid |
⊢ ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → 𝑐 ⊆ ( 𝑅1 ‘ 𝑏 ) ) |
56 |
|
resima2 |
⊢ ( 𝑐 ⊆ ( 𝑅1 ‘ 𝑏 ) → ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑐 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑐 ) ) |
57 |
55 56
|
syl |
⊢ ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑐 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑐 ) ) |
58 |
57
|
fveq2d |
⊢ ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑐 ) ) = ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑐 ) ) ) |
59 |
|
fvex |
⊢ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ∈ V |
60 |
59
|
resex |
⊢ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ∈ V |
61 |
|
dmeq |
⊢ ( 𝑥 = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) → dom 𝑥 = dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) |
62 |
61
|
pweqd |
⊢ ( 𝑥 = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) → 𝒫 dom 𝑥 = 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) |
63 |
|
imaeq1 |
⊢ ( 𝑥 = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) → ( 𝑥 “ 𝑦 ) = ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑦 ) ) |
64 |
63
|
fveq2d |
⊢ ( 𝑥 = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) → ( 𝐹 ‘ ( 𝑥 “ 𝑦 ) ) = ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑦 ) ) ) |
65 |
62 64
|
mpteq12dv |
⊢ ( 𝑥 = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) → ( 𝑦 ∈ 𝒫 dom 𝑥 ↦ ( 𝐹 ‘ ( 𝑥 “ 𝑦 ) ) ) = ( 𝑦 ∈ 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ↦ ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑦 ) ) ) ) |
66 |
60
|
dmex |
⊢ dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ∈ V |
67 |
66
|
pwex |
⊢ 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ∈ V |
68 |
67
|
mptex |
⊢ ( 𝑦 ∈ 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ↦ ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑦 ) ) ) ∈ V |
69 |
65 2 68
|
fvmpt |
⊢ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ∈ V → ( 𝐺 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) = ( 𝑦 ∈ 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ↦ ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑦 ) ) ) ) |
70 |
60 69
|
ax-mp |
⊢ ( 𝐺 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) = ( 𝑦 ∈ 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ↦ ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑦 ) ) ) |
71 |
70
|
fveq1i |
⊢ ( ( 𝐺 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) ‘ 𝑐 ) = ( ( 𝑦 ∈ 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ↦ ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑦 ) ) ) ‘ 𝑐 ) |
72 |
|
r1sssuc |
⊢ ( 𝑏 ∈ On → ( 𝑅1 ‘ 𝑏 ) ⊆ ( 𝑅1 ‘ suc 𝑏 ) ) |
73 |
50 72
|
syl |
⊢ ( 𝑏 ∈ ω → ( 𝑅1 ‘ 𝑏 ) ⊆ ( 𝑅1 ‘ suc 𝑏 ) ) |
74 |
|
fnssres |
⊢ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) Fn ( 𝑅1 ‘ suc 𝑏 ) ∧ ( 𝑅1 ‘ 𝑏 ) ⊆ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) Fn ( 𝑅1 ‘ 𝑏 ) ) |
75 |
37 73 74
|
syl2anc |
⊢ ( 𝑏 ∈ ω → ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) Fn ( 𝑅1 ‘ 𝑏 ) ) |
76 |
75
|
fndmd |
⊢ ( 𝑏 ∈ ω → dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) = ( 𝑅1 ‘ 𝑏 ) ) |
77 |
76
|
pweqd |
⊢ ( 𝑏 ∈ ω → 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) = 𝒫 ( 𝑅1 ‘ 𝑏 ) ) |
78 |
77
|
adantr |
⊢ ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) = 𝒫 ( 𝑅1 ‘ 𝑏 ) ) |
79 |
54 78
|
eleqtrrd |
⊢ ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → 𝑐 ∈ 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) |
80 |
|
imaeq2 |
⊢ ( 𝑦 = 𝑐 → ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑦 ) = ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑐 ) ) |
81 |
80
|
fveq2d |
⊢ ( 𝑦 = 𝑐 → ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑦 ) ) = ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑐 ) ) ) |
82 |
|
eqid |
⊢ ( 𝑦 ∈ 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ↦ ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑦 ) ) ) = ( 𝑦 ∈ 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ↦ ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑦 ) ) ) |
83 |
|
fvex |
⊢ ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑐 ) ) ∈ V |
84 |
81 82 83
|
fvmpt |
⊢ ( 𝑐 ∈ 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) → ( ( 𝑦 ∈ 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ↦ ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑦 ) ) ) ‘ 𝑐 ) = ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑐 ) ) ) |
85 |
79 84
|
syl |
⊢ ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( 𝑦 ∈ 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ↦ ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑦 ) ) ) ‘ 𝑐 ) = ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑐 ) ) ) |
86 |
71 85
|
eqtrid |
⊢ ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( 𝐺 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) ‘ 𝑐 ) = ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑐 ) ) ) |
87 |
|
dmeq |
⊢ ( 𝑥 = ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) → dom 𝑥 = dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) |
88 |
87
|
pweqd |
⊢ ( 𝑥 = ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) → 𝒫 dom 𝑥 = 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) |
89 |
|
imaeq1 |
⊢ ( 𝑥 = ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) → ( 𝑥 “ 𝑦 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) |
90 |
89
|
fveq2d |
⊢ ( 𝑥 = ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) → ( 𝐹 ‘ ( 𝑥 “ 𝑦 ) ) = ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) ) |
91 |
88 90
|
mpteq12dv |
⊢ ( 𝑥 = ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) → ( 𝑦 ∈ 𝒫 dom 𝑥 ↦ ( 𝐹 ‘ ( 𝑥 “ 𝑦 ) ) ) = ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) ) ) |
92 |
59
|
dmex |
⊢ dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ∈ V |
93 |
92
|
pwex |
⊢ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ∈ V |
94 |
93
|
mptex |
⊢ ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) ) ∈ V |
95 |
91 2 94
|
fvmpt |
⊢ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ∈ V → ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) = ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) ) ) |
96 |
59 95
|
ax-mp |
⊢ ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) = ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) ) |
97 |
96
|
fveq1i |
⊢ ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) ‘ 𝑐 ) = ( ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) ) ‘ 𝑐 ) |
98 |
|
r1tr |
⊢ Tr ( 𝑅1 ‘ suc 𝑏 ) |
99 |
98
|
a1i |
⊢ ( 𝑏 ∈ ω → Tr ( 𝑅1 ‘ suc 𝑏 ) ) |
100 |
|
dftr4 |
⊢ ( Tr ( 𝑅1 ‘ suc 𝑏 ) ↔ ( 𝑅1 ‘ suc 𝑏 ) ⊆ 𝒫 ( 𝑅1 ‘ suc 𝑏 ) ) |
101 |
99 100
|
sylib |
⊢ ( 𝑏 ∈ ω → ( 𝑅1 ‘ suc 𝑏 ) ⊆ 𝒫 ( 𝑅1 ‘ suc 𝑏 ) ) |
102 |
101
|
sselda |
⊢ ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → 𝑐 ∈ 𝒫 ( 𝑅1 ‘ suc 𝑏 ) ) |
103 |
|
f1odm |
⊢ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) : ( 𝑅1 ‘ suc 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) → dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = ( 𝑅1 ‘ suc 𝑏 ) ) |
104 |
35 103
|
syl |
⊢ ( 𝑏 ∈ ω → dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = ( 𝑅1 ‘ suc 𝑏 ) ) |
105 |
104
|
pweqd |
⊢ ( 𝑏 ∈ ω → 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = 𝒫 ( 𝑅1 ‘ suc 𝑏 ) ) |
106 |
105
|
adantr |
⊢ ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = 𝒫 ( 𝑅1 ‘ suc 𝑏 ) ) |
107 |
102 106
|
eleqtrrd |
⊢ ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → 𝑐 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) |
108 |
|
imaeq2 |
⊢ ( 𝑦 = 𝑐 → ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑐 ) ) |
109 |
108
|
fveq2d |
⊢ ( 𝑦 = 𝑐 → ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) = ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑐 ) ) ) |
110 |
|
eqid |
⊢ ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) ) = ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) ) |
111 |
|
fvex |
⊢ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑐 ) ) ∈ V |
112 |
109 110 111
|
fvmpt |
⊢ ( 𝑐 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) → ( ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) ) ‘ 𝑐 ) = ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑐 ) ) ) |
113 |
107 112
|
syl |
⊢ ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) ) ‘ 𝑐 ) = ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑐 ) ) ) |
114 |
97 113
|
eqtrid |
⊢ ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) ‘ 𝑐 ) = ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑐 ) ) ) |
115 |
58 86 114
|
3eqtr4d |
⊢ ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( 𝐺 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) ‘ 𝑐 ) = ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) ‘ 𝑐 ) ) |
116 |
115
|
adantlr |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( 𝐺 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) ‘ 𝑐 ) = ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) ‘ 𝑐 ) ) |
117 |
|
fveq2 |
⊢ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) → ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) = ( 𝐺 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) ) |
118 |
117
|
fveq1d |
⊢ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) → ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) ‘ 𝑐 ) = ( ( 𝐺 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) ‘ 𝑐 ) ) |
119 |
118
|
ad2antlr |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) ‘ 𝑐 ) = ( ( 𝐺 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) ‘ 𝑐 ) ) |
120 |
|
rdgsuc |
⊢ ( suc 𝑏 ∈ On → ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) = ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) ) |
121 |
44 120
|
syl |
⊢ ( 𝑏 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) = ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) ) |
122 |
121
|
fveq1d |
⊢ ( 𝑏 ∈ ω → ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ‘ 𝑐 ) = ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) ‘ 𝑐 ) ) |
123 |
122
|
ad2antrr |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ‘ 𝑐 ) = ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) ‘ 𝑐 ) ) |
124 |
116 119 123
|
3eqtr4rd |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ‘ 𝑐 ) = ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) ‘ 𝑐 ) ) |
125 |
|
fvres |
⊢ ( 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) → ( ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ↾ ( 𝑅1 ‘ suc 𝑏 ) ) ‘ 𝑐 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ‘ 𝑐 ) ) |
126 |
125
|
adantl |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ↾ ( 𝑅1 ‘ suc 𝑏 ) ) ‘ 𝑐 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ‘ 𝑐 ) ) |
127 |
|
rdgsuc |
⊢ ( 𝑏 ∈ On → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) ) |
128 |
50 127
|
syl |
⊢ ( 𝑏 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) ) |
129 |
128
|
fveq1d |
⊢ ( 𝑏 ∈ ω → ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ‘ 𝑐 ) = ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) ‘ 𝑐 ) ) |
130 |
129
|
ad2antrr |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ‘ 𝑐 ) = ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) ‘ 𝑐 ) ) |
131 |
124 126 130
|
3eqtr4rd |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ‘ 𝑐 ) = ( ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ↾ ( 𝑅1 ‘ suc 𝑏 ) ) ‘ 𝑐 ) ) |
132 |
38 49 131
|
eqfnfvd |
⊢ ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ↾ ( 𝑅1 ‘ suc 𝑏 ) ) ) |
133 |
132
|
ex |
⊢ ( 𝑏 ∈ ω → ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ↾ ( 𝑅1 ‘ suc 𝑏 ) ) ) ) |
134 |
8 14 20 26 32 133
|
finds |
⊢ ( 𝐴 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ 𝐴 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝐴 ) ↾ ( 𝑅1 ‘ 𝐴 ) ) ) |
135 |
|
resss |
⊢ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝐴 ) ↾ ( 𝑅1 ‘ 𝐴 ) ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ suc 𝐴 ) |
136 |
134 135
|
eqsstrdi |
⊢ ( 𝐴 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ 𝐴 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ suc 𝐴 ) ) |