Step | Hyp | Ref
| Expression |
1 | | cantnfvalf.f |
. . 3
β’ πΉ = seqΟ((π β π΄, π§ β π΅ β¦ (πΆ +o π·)), β
) |
2 | 1 | fnseqom 8405 |
. 2
β’ πΉ Fn Ο |
3 | | nn0suc 7836 |
. . . 4
β’ (π₯ β Ο β (π₯ = β
β¨ βπ¦ β Ο π₯ = suc π¦)) |
4 | | fveq2 6846 |
. . . . . . 7
β’ (π₯ = β
β (πΉβπ₯) = (πΉββ
)) |
5 | | 0ex 5268 |
. . . . . . . 8
β’ β
β V |
6 | 1 | seqom0g 8406 |
. . . . . . . 8
β’ (β
β V β (πΉββ
) = β
) |
7 | 5, 6 | ax-mp 5 |
. . . . . . 7
β’ (πΉββ
) =
β
|
8 | 4, 7 | eqtrdi 2789 |
. . . . . 6
β’ (π₯ = β
β (πΉβπ₯) = β
) |
9 | | 0elon 6375 |
. . . . . 6
β’ β
β On |
10 | 8, 9 | eqeltrdi 2842 |
. . . . 5
β’ (π₯ = β
β (πΉβπ₯) β On) |
11 | 1 | seqomsuc 8407 |
. . . . . . . . 9
β’ (π¦ β Ο β (πΉβsuc π¦) = (π¦(π β π΄, π§ β π΅ β¦ (πΆ +o π·))(πΉβπ¦))) |
12 | | df-ov 7364 |
. . . . . . . . 9
β’ (π¦(π β π΄, π§ β π΅ β¦ (πΆ +o π·))(πΉβπ¦)) = ((π β π΄, π§ β π΅ β¦ (πΆ +o π·))ββ¨π¦, (πΉβπ¦)β©) |
13 | 11, 12 | eqtrdi 2789 |
. . . . . . . 8
β’ (π¦ β Ο β (πΉβsuc π¦) = ((π β π΄, π§ β π΅ β¦ (πΆ +o π·))ββ¨π¦, (πΉβπ¦)β©)) |
14 | | df-ov 7364 |
. . . . . . . . . . . 12
β’ (πΆ +o π·) = ( +o ββ¨πΆ, π·β©) |
15 | | fnoa 8458 |
. . . . . . . . . . . . . 14
β’
+o Fn (On Γ On) |
16 | | oacl 8485 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β On β§ π¦ β On) β (π₯ +o π¦) β On) |
17 | 16 | rgen2 3191 |
. . . . . . . . . . . . . 14
β’
βπ₯ β On
βπ¦ β On (π₯ +o π¦) β On |
18 | | ffnov 7487 |
. . . . . . . . . . . . . 14
β’ (
+o :(On Γ On)βΆOn β ( +o Fn (On Γ
On) β§ βπ₯ β
On βπ¦ β On
(π₯ +o π¦) β On)) |
19 | 15, 17, 18 | mpbir2an 710 |
. . . . . . . . . . . . 13
β’
+o :(On Γ On)βΆOn |
20 | 19, 9 | f0cli 7052 |
. . . . . . . . . . . 12
β’ (
+o ββ¨πΆ, π·β©) β On |
21 | 14, 20 | eqeltri 2830 |
. . . . . . . . . . 11
β’ (πΆ +o π·) β On |
22 | 21 | rgen2w 3066 |
. . . . . . . . . 10
β’
βπ β
π΄ βπ§ β π΅ (πΆ +o π·) β On |
23 | | eqid 2733 |
. . . . . . . . . . 11
β’ (π β π΄, π§ β π΅ β¦ (πΆ +o π·)) = (π β π΄, π§ β π΅ β¦ (πΆ +o π·)) |
24 | 23 | fmpo 8004 |
. . . . . . . . . 10
β’
(βπ β
π΄ βπ§ β π΅ (πΆ +o π·) β On β (π β π΄, π§ β π΅ β¦ (πΆ +o π·)):(π΄ Γ π΅)βΆOn) |
25 | 22, 24 | mpbi 229 |
. . . . . . . . 9
β’ (π β π΄, π§ β π΅ β¦ (πΆ +o π·)):(π΄ Γ π΅)βΆOn |
26 | 25, 9 | f0cli 7052 |
. . . . . . . 8
β’ ((π β π΄, π§ β π΅ β¦ (πΆ +o π·))ββ¨π¦, (πΉβπ¦)β©) β On |
27 | 13, 26 | eqeltrdi 2842 |
. . . . . . 7
β’ (π¦ β Ο β (πΉβsuc π¦) β On) |
28 | | fveq2 6846 |
. . . . . . . 8
β’ (π₯ = suc π¦ β (πΉβπ₯) = (πΉβsuc π¦)) |
29 | 28 | eleq1d 2819 |
. . . . . . 7
β’ (π₯ = suc π¦ β ((πΉβπ₯) β On β (πΉβsuc π¦) β On)) |
30 | 27, 29 | syl5ibrcom 247 |
. . . . . 6
β’ (π¦ β Ο β (π₯ = suc π¦ β (πΉβπ₯) β On)) |
31 | 30 | rexlimiv 3142 |
. . . . 5
β’
(βπ¦ β
Ο π₯ = suc π¦ β (πΉβπ₯) β On) |
32 | 10, 31 | jaoi 856 |
. . . 4
β’ ((π₯ = β
β¨ βπ¦ β Ο π₯ = suc π¦) β (πΉβπ₯) β On) |
33 | 3, 32 | syl 17 |
. . 3
β’ (π₯ β Ο β (πΉβπ₯) β On) |
34 | 33 | rgen 3063 |
. 2
β’
βπ₯ β
Ο (πΉβπ₯) β On |
35 | | ffnfv 7070 |
. 2
β’ (πΉ:ΟβΆOn β (πΉ Fn Ο β§ βπ₯ β Ο (πΉβπ₯) β On)) |
36 | 2, 34, 35 | mpbir2an 710 |
1
β’ πΉ:ΟβΆOn |