Step | Hyp | Ref
| Expression |
1 | | tfrlem.1 |
. . . . . 6
β’ π΄ = {π β£ βπ₯ β On (π Fn π₯ β§ βπ¦ β π₯ (πβπ¦) = (πΉβ(π βΎ π¦)))} |
2 | 1 | tfrlem8 8383 |
. . . . 5
β’ Ord dom
recs(πΉ) |
3 | 2 | a1i 11 |
. . . 4
β’
(recs(πΉ) β V
β Ord dom recs(πΉ)) |
4 | | dmexg 7893 |
. . . 4
β’
(recs(πΉ) β V
β dom recs(πΉ) β
V) |
5 | | elon2 6375 |
. . . 4
β’ (dom
recs(πΉ) β On β
(Ord dom recs(πΉ) β§ dom
recs(πΉ) β
V)) |
6 | 3, 4, 5 | sylanbrc 583 |
. . 3
β’
(recs(πΉ) β V
β dom recs(πΉ) β
On) |
7 | | onsuc 7798 |
. . . 4
β’ (dom
recs(πΉ) β On β
suc dom recs(πΉ) β
On) |
8 | | tfrlem.3 |
. . . . 5
β’ πΆ = (recs(πΉ) βͺ {β¨dom recs(πΉ), (πΉβrecs(πΉ))β©}) |
9 | 1, 8 | tfrlem10 8386 |
. . . 4
β’ (dom
recs(πΉ) β On β
πΆ Fn suc dom recs(πΉ)) |
10 | 1, 8 | tfrlem11 8387 |
. . . . . 6
β’ (dom
recs(πΉ) β On β
(π§ β suc dom
recs(πΉ) β (πΆβπ§) = (πΉβ(πΆ βΎ π§)))) |
11 | 10 | ralrimiv 3145 |
. . . . 5
β’ (dom
recs(πΉ) β On β
βπ§ β suc dom
recs(πΉ)(πΆβπ§) = (πΉβ(πΆ βΎ π§))) |
12 | | fveq2 6891 |
. . . . . . 7
β’ (π§ = π¦ β (πΆβπ§) = (πΆβπ¦)) |
13 | | reseq2 5976 |
. . . . . . . 8
β’ (π§ = π¦ β (πΆ βΎ π§) = (πΆ βΎ π¦)) |
14 | 13 | fveq2d 6895 |
. . . . . . 7
β’ (π§ = π¦ β (πΉβ(πΆ βΎ π§)) = (πΉβ(πΆ βΎ π¦))) |
15 | 12, 14 | eqeq12d 2748 |
. . . . . 6
β’ (π§ = π¦ β ((πΆβπ§) = (πΉβ(πΆ βΎ π§)) β (πΆβπ¦) = (πΉβ(πΆ βΎ π¦)))) |
16 | 15 | cbvralvw 3234 |
. . . . 5
β’
(βπ§ β
suc dom recs(πΉ)(πΆβπ§) = (πΉβ(πΆ βΎ π§)) β βπ¦ β suc dom recs(πΉ)(πΆβπ¦) = (πΉβ(πΆ βΎ π¦))) |
17 | 11, 16 | sylib 217 |
. . . 4
β’ (dom
recs(πΉ) β On β
βπ¦ β suc dom
recs(πΉ)(πΆβπ¦) = (πΉβ(πΆ βΎ π¦))) |
18 | | fneq2 6641 |
. . . . . 6
β’ (π₯ = suc dom recs(πΉ) β (πΆ Fn π₯ β πΆ Fn suc dom recs(πΉ))) |
19 | | raleq 3322 |
. . . . . 6
β’ (π₯ = suc dom recs(πΉ) β (βπ¦ β π₯ (πΆβπ¦) = (πΉβ(πΆ βΎ π¦)) β βπ¦ β suc dom recs(πΉ)(πΆβπ¦) = (πΉβ(πΆ βΎ π¦)))) |
20 | 18, 19 | anbi12d 631 |
. . . . 5
β’ (π₯ = suc dom recs(πΉ) β ((πΆ Fn π₯ β§ βπ¦ β π₯ (πΆβπ¦) = (πΉβ(πΆ βΎ π¦))) β (πΆ Fn suc dom recs(πΉ) β§ βπ¦ β suc dom recs(πΉ)(πΆβπ¦) = (πΉβ(πΆ βΎ π¦))))) |
21 | 20 | rspcev 3612 |
. . . 4
β’ ((suc dom
recs(πΉ) β On β§
(πΆ Fn suc dom recs(πΉ) β§ βπ¦ β suc dom recs(πΉ)(πΆβπ¦) = (πΉβ(πΆ βΎ π¦)))) β βπ₯ β On (πΆ Fn π₯ β§ βπ¦ β π₯ (πΆβπ¦) = (πΉβ(πΆ βΎ π¦)))) |
22 | 7, 9, 17, 21 | syl12anc 835 |
. . 3
β’ (dom
recs(πΉ) β On β
βπ₯ β On (πΆ Fn π₯ β§ βπ¦ β π₯ (πΆβπ¦) = (πΉβ(πΆ βΎ π¦)))) |
23 | 6, 22 | syl 17 |
. 2
β’
(recs(πΉ) β V
β βπ₯ β On
(πΆ Fn π₯ β§ βπ¦ β π₯ (πΆβπ¦) = (πΉβ(πΆ βΎ π¦)))) |
24 | | snex 5431 |
. . . . 5
β’
{β¨dom recs(πΉ),
(πΉβrecs(πΉ))β©} β
V |
25 | | unexg 7735 |
. . . . 5
β’
((recs(πΉ) β V
β§ {β¨dom recs(πΉ),
(πΉβrecs(πΉ))β©} β V) β
(recs(πΉ) βͺ {β¨dom
recs(πΉ), (πΉβrecs(πΉ))β©}) β V) |
26 | 24, 25 | mpan2 689 |
. . . 4
β’
(recs(πΉ) β V
β (recs(πΉ) βͺ
{β¨dom recs(πΉ), (πΉβrecs(πΉ))β©}) β V) |
27 | 8, 26 | eqeltrid 2837 |
. . 3
β’
(recs(πΉ) β V
β πΆ β
V) |
28 | | fneq1 6640 |
. . . . . 6
β’ (π = πΆ β (π Fn π₯ β πΆ Fn π₯)) |
29 | | fveq1 6890 |
. . . . . . . 8
β’ (π = πΆ β (πβπ¦) = (πΆβπ¦)) |
30 | | reseq1 5975 |
. . . . . . . . 9
β’ (π = πΆ β (π βΎ π¦) = (πΆ βΎ π¦)) |
31 | 30 | fveq2d 6895 |
. . . . . . . 8
β’ (π = πΆ β (πΉβ(π βΎ π¦)) = (πΉβ(πΆ βΎ π¦))) |
32 | 29, 31 | eqeq12d 2748 |
. . . . . . 7
β’ (π = πΆ β ((πβπ¦) = (πΉβ(π βΎ π¦)) β (πΆβπ¦) = (πΉβ(πΆ βΎ π¦)))) |
33 | 32 | ralbidv 3177 |
. . . . . 6
β’ (π = πΆ β (βπ¦ β π₯ (πβπ¦) = (πΉβ(π βΎ π¦)) β βπ¦ β π₯ (πΆβπ¦) = (πΉβ(πΆ βΎ π¦)))) |
34 | 28, 33 | anbi12d 631 |
. . . . 5
β’ (π = πΆ β ((π Fn π₯ β§ βπ¦ β π₯ (πβπ¦) = (πΉβ(π βΎ π¦))) β (πΆ Fn π₯ β§ βπ¦ β π₯ (πΆβπ¦) = (πΉβ(πΆ βΎ π¦))))) |
35 | 34 | rexbidv 3178 |
. . . 4
β’ (π = πΆ β (βπ₯ β On (π Fn π₯ β§ βπ¦ β π₯ (πβπ¦) = (πΉβ(π βΎ π¦))) β βπ₯ β On (πΆ Fn π₯ β§ βπ¦ β π₯ (πΆβπ¦) = (πΉβ(πΆ βΎ π¦))))) |
36 | 35, 1 | elab2g 3670 |
. . 3
β’ (πΆ β V β (πΆ β π΄ β βπ₯ β On (πΆ Fn π₯ β§ βπ¦ β π₯ (πΆβπ¦) = (πΉβ(πΆ βΎ π¦))))) |
37 | 27, 36 | syl 17 |
. 2
β’
(recs(πΉ) β V
β (πΆ β π΄ β βπ₯ β On (πΆ Fn π₯ β§ βπ¦ β π₯ (πΆβπ¦) = (πΉβ(πΆ βΎ π¦))))) |
38 | 23, 37 | mpbird 256 |
1
β’
(recs(πΉ) β V
β πΆ β π΄) |