Step | Hyp | Ref
| Expression |
1 | | df-irdg 6370 |
. 2
β’ rec(πΉ, π΄) = recs((π β V β¦ (π΄ βͺ βͺ
π₯ β dom π(πΉβ(πβπ₯))))) |
2 | | funmpt 5254 |
. . 3
β’ Fun
(π β V β¦ (π΄ βͺ βͺ π₯ β dom π(πΉβ(πβπ₯)))) |
3 | 2 | a1i 9 |
. 2
β’ ((π β§ π΅ β On) β Fun (π β V β¦ (π΄ βͺ βͺ
π₯ β dom π(πΉβ(πβπ₯))))) |
4 | | ordon 4485 |
. . 3
β’ Ord
On |
5 | 4 | a1i 9 |
. 2
β’ ((π β§ π΅ β On) β Ord On) |
6 | | vex 2740 |
. . . 4
β’ π β V |
7 | | rdgon.2 |
. . . . . . 7
β’ (π β π΄ β On) |
8 | 7 | adantr 276 |
. . . . . 6
β’ ((π β§ π΅ β On) β π΄ β On) |
9 | 8 | 3ad2ant1 1018 |
. . . . 5
β’ (((π β§ π΅ β On) β§ π¦ β On β§ π:π¦βΆOn) β π΄ β On) |
10 | 6 | dmex 4893 |
. . . . . 6
β’ dom π β V |
11 | | fveq2 5515 |
. . . . . . . . . 10
β’ (π₯ = (πβπ§) β (πΉβπ₯) = (πΉβ(πβπ§))) |
12 | 11 | eleq1d 2246 |
. . . . . . . . 9
β’ (π₯ = (πβπ§) β ((πΉβπ₯) β On β (πΉβ(πβπ§)) β On)) |
13 | | rdgon.3 |
. . . . . . . . . . . 12
β’ (π β βπ₯ β On (πΉβπ₯) β On) |
14 | 13 | adantr 276 |
. . . . . . . . . . 11
β’ ((π β§ π΅ β On) β βπ₯ β On (πΉβπ₯) β On) |
15 | 14 | 3ad2ant1 1018 |
. . . . . . . . . 10
β’ (((π β§ π΅ β On) β§ π¦ β On β§ π:π¦βΆOn) β βπ₯ β On (πΉβπ₯) β On) |
16 | 15 | adantr 276 |
. . . . . . . . 9
β’ ((((π β§ π΅ β On) β§ π¦ β On β§ π:π¦βΆOn) β§ π§ β dom π) β βπ₯ β On (πΉβπ₯) β On) |
17 | | simpl3 1002 |
. . . . . . . . . 10
β’ ((((π β§ π΅ β On) β§ π¦ β On β§ π:π¦βΆOn) β§ π§ β dom π) β π:π¦βΆOn) |
18 | | simpr 110 |
. . . . . . . . . . 11
β’ ((((π β§ π΅ β On) β§ π¦ β On β§ π:π¦βΆOn) β§ π§ β dom π) β π§ β dom π) |
19 | | fdm 5371 |
. . . . . . . . . . . . 13
β’ (π:π¦βΆOn β dom π = π¦) |
20 | 19 | eleq2d 2247 |
. . . . . . . . . . . 12
β’ (π:π¦βΆOn β (π§ β dom π β π§ β π¦)) |
21 | 17, 20 | syl 14 |
. . . . . . . . . . 11
β’ ((((π β§ π΅ β On) β§ π¦ β On β§ π:π¦βΆOn) β§ π§ β dom π) β (π§ β dom π β π§ β π¦)) |
22 | 18, 21 | mpbid 147 |
. . . . . . . . . 10
β’ ((((π β§ π΅ β On) β§ π¦ β On β§ π:π¦βΆOn) β§ π§ β dom π) β π§ β π¦) |
23 | 17, 22 | ffvelcdmd 5652 |
. . . . . . . . 9
β’ ((((π β§ π΅ β On) β§ π¦ β On β§ π:π¦βΆOn) β§ π§ β dom π) β (πβπ§) β On) |
24 | 12, 16, 23 | rspcdva 2846 |
. . . . . . . 8
β’ ((((π β§ π΅ β On) β§ π¦ β On β§ π:π¦βΆOn) β§ π§ β dom π) β (πΉβ(πβπ§)) β On) |
25 | 24 | ralrimiva 2550 |
. . . . . . 7
β’ (((π β§ π΅ β On) β§ π¦ β On β§ π:π¦βΆOn) β βπ§ β dom π(πΉβ(πβπ§)) β On) |
26 | | fveq2 5515 |
. . . . . . . . . 10
β’ (π₯ = π§ β (πβπ₯) = (πβπ§)) |
27 | 26 | fveq2d 5519 |
. . . . . . . . 9
β’ (π₯ = π§ β (πΉβ(πβπ₯)) = (πΉβ(πβπ§))) |
28 | 27 | eleq1d 2246 |
. . . . . . . 8
β’ (π₯ = π§ β ((πΉβ(πβπ₯)) β On β (πΉβ(πβπ§)) β On)) |
29 | 28 | cbvralv 2703 |
. . . . . . 7
β’
(βπ₯ β
dom π(πΉβ(πβπ₯)) β On β βπ§ β dom π(πΉβ(πβπ§)) β On) |
30 | 25, 29 | sylibr 134 |
. . . . . 6
β’ (((π β§ π΅ β On) β§ π¦ β On β§ π:π¦βΆOn) β βπ₯ β dom π(πΉβ(πβπ₯)) β On) |
31 | | iunon 6284 |
. . . . . 6
β’ ((dom
π β V β§
βπ₯ β dom π(πΉβ(πβπ₯)) β On) β βͺ π₯ β dom π(πΉβ(πβπ₯)) β On) |
32 | 10, 30, 31 | sylancr 414 |
. . . . 5
β’ (((π β§ π΅ β On) β§ π¦ β On β§ π:π¦βΆOn) β βͺ π₯ β dom π(πΉβ(πβπ₯)) β On) |
33 | | onun2 4489 |
. . . . 5
β’ ((π΄ β On β§ βͺ π₯ β dom π(πΉβ(πβπ₯)) β On) β (π΄ βͺ βͺ
π₯ β dom π(πΉβ(πβπ₯))) β On) |
34 | 9, 32, 33 | syl2anc 411 |
. . . 4
β’ (((π β§ π΅ β On) β§ π¦ β On β§ π:π¦βΆOn) β (π΄ βͺ βͺ
π₯ β dom π(πΉβ(πβπ₯))) β On) |
35 | | dmeq 4827 |
. . . . . . 7
β’ (π = π β dom π = dom π) |
36 | | fveq1 5514 |
. . . . . . . 8
β’ (π = π β (πβπ₯) = (πβπ₯)) |
37 | 36 | fveq2d 5519 |
. . . . . . 7
β’ (π = π β (πΉβ(πβπ₯)) = (πΉβ(πβπ₯))) |
38 | 35, 37 | iuneq12d 3910 |
. . . . . 6
β’ (π = π β βͺ
π₯ β dom π(πΉβ(πβπ₯)) = βͺ
π₯ β dom π(πΉβ(πβπ₯))) |
39 | 38 | uneq2d 3289 |
. . . . 5
β’ (π = π β (π΄ βͺ βͺ
π₯ β dom π(πΉβ(πβπ₯))) = (π΄ βͺ βͺ
π₯ β dom π(πΉβ(πβπ₯)))) |
40 | | eqid 2177 |
. . . . 5
β’ (π β V β¦ (π΄ βͺ βͺ π₯ β dom π(πΉβ(πβπ₯)))) = (π β V β¦ (π΄ βͺ βͺ
π₯ β dom π(πΉβ(πβπ₯)))) |
41 | 39, 40 | fvmptg 5592 |
. . . 4
β’ ((π β V β§ (π΄ βͺ βͺ π₯ β dom π(πΉβ(πβπ₯))) β On) β ((π β V β¦ (π΄ βͺ βͺ
π₯ β dom π(πΉβ(πβπ₯))))βπ) = (π΄ βͺ βͺ
π₯ β dom π(πΉβ(πβπ₯)))) |
42 | 6, 34, 41 | sylancr 414 |
. . 3
β’ (((π β§ π΅ β On) β§ π¦ β On β§ π:π¦βΆOn) β ((π β V β¦ (π΄ βͺ βͺ
π₯ β dom π(πΉβ(πβπ₯))))βπ) = (π΄ βͺ βͺ
π₯ β dom π(πΉβ(πβπ₯)))) |
43 | 42, 34 | eqeltrd 2254 |
. 2
β’ (((π β§ π΅ β On) β§ π¦ β On β§ π:π¦βΆOn) β ((π β V β¦ (π΄ βͺ βͺ
π₯ β dom π(πΉβ(πβπ₯))))βπ) β On) |
44 | | unon 4510 |
. . . . . 6
β’ βͺ On = On |
45 | 44 | eleq2i 2244 |
. . . . 5
β’ (π¦ β βͺ On β π¦ β On) |
46 | 45 | biimpi 120 |
. . . 4
β’ (π¦ β βͺ On β π¦ β On) |
47 | 46 | adantl 277 |
. . 3
β’ (((π β§ π΅ β On) β§ π¦ β βͺ On)
β π¦ β
On) |
48 | | onsuc 4500 |
. . 3
β’ (π¦ β On β suc π¦ β On) |
49 | 47, 48 | syl 14 |
. 2
β’ (((π β§ π΅ β On) β§ π¦ β βͺ On)
β suc π¦ β
On) |
50 | 44 | eleq2i 2244 |
. . . 4
β’ (π΅ β βͺ On β π΅ β On) |
51 | 50 | biimpri 133 |
. . 3
β’ (π΅ β On β π΅ β βͺ On) |
52 | 51 | adantl 277 |
. 2
β’ ((π β§ π΅ β On) β π΅ β βͺ
On) |
53 | 1, 3, 5, 43, 49, 52 | tfrcl 6364 |
1
β’ ((π β§ π΅ β On) β (rec(πΉ, π΄)βπ΅) β On) |