Step | Hyp | Ref
| Expression |
1 | | cnfcom3c 9649 |
. 2
β’ (π΄ β On β βπβπ₯ β π΄ (Ο β π₯ β βπ¦ β (On β 1o)(πβπ₯):π₯β1-1-ontoβ(Ο βo π¦))) |
2 | | df-2o 8418 |
. . . . . . . 8
β’
2o = suc 1o |
3 | 2 | oveq2i 7373 |
. . . . . . 7
β’ (Ο
βo 2o) = (Ο βo suc
1o) |
4 | | omelon 9589 |
. . . . . . . 8
β’ Ο
β On |
5 | | 1on 8429 |
. . . . . . . 8
β’
1o β On |
6 | | oesuc 8478 |
. . . . . . . 8
β’ ((Ο
β On β§ 1o β On) β (Ο βo suc
1o) = ((Ο βo 1o)
Β·o Ο)) |
7 | 4, 5, 6 | mp2an 691 |
. . . . . . 7
β’ (Ο
βo suc 1o) = ((Ο βo
1o) Β·o Ο) |
8 | | oe1 8496 |
. . . . . . . . 9
β’ (Ο
β On β (Ο βo 1o) =
Ο) |
9 | 4, 8 | ax-mp 5 |
. . . . . . . 8
β’ (Ο
βo 1o) = Ο |
10 | 9 | oveq1i 7372 |
. . . . . . 7
β’ ((Ο
βo 1o) Β·o Ο) = (Ο
Β·o Ο) |
11 | 3, 7, 10 | 3eqtri 2769 |
. . . . . 6
β’ (Ο
βo 2o) = (Ο Β·o
Ο) |
12 | | omxpen 9025 |
. . . . . . 7
β’ ((Ο
β On β§ Ο β On) β (Ο Β·o
Ο) β (Ο Γ Ο)) |
13 | 4, 4, 12 | mp2an 691 |
. . . . . 6
β’ (Ο
Β·o Ο) β (Ο Γ
Ο) |
14 | 11, 13 | eqbrtri 5131 |
. . . . 5
β’ (Ο
βo 2o) β (Ο Γ
Ο) |
15 | | xpomen 9958 |
. . . . 5
β’ (Ο
Γ Ο) β Ο |
16 | 14, 15 | entri 8955 |
. . . 4
β’ (Ο
βo 2o) β Ο |
17 | 16 | a1i 11 |
. . 3
β’ (π΄ β On β (Ο
βo 2o) β Ο) |
18 | | bren 8900 |
. . 3
β’ ((Ο
βo 2o) β Ο β βπ π:(Ο βo
2o)β1-1-ontoβΟ) |
19 | 17, 18 | sylib 217 |
. 2
β’ (π΄ β On β βπ π:(Ο βo
2o)β1-1-ontoβΟ) |
20 | | exdistrv 1960 |
. . 3
β’
(βπβπ(βπ₯ β π΄ (Ο β π₯ β βπ¦ β (On β 1o)(πβπ₯):π₯β1-1-ontoβ(Ο βo π¦)) β§ π:(Ο βo
2o)β1-1-ontoβΟ) β (βπβπ₯ β π΄ (Ο β π₯ β βπ¦ β (On β 1o)(πβπ₯):π₯β1-1-ontoβ(Ο βo π¦)) β§ βπ π:(Ο βo
2o)β1-1-ontoβΟ)) |
21 | | simpl 484 |
. . . . . 6
β’ ((π΄ β On β§ (βπ₯ β π΄ (Ο β π₯ β βπ¦ β (On β 1o)(πβπ₯):π₯β1-1-ontoβ(Ο βo π¦)) β§ π:(Ο βo
2o)β1-1-ontoβΟ)) β π΄ β On) |
22 | | simprl 770 |
. . . . . . 7
β’ ((π΄ β On β§ (βπ₯ β π΄ (Ο β π₯ β βπ¦ β (On β 1o)(πβπ₯):π₯β1-1-ontoβ(Ο βo π¦)) β§ π:(Ο βo
2o)β1-1-ontoβΟ)) β βπ₯ β π΄ (Ο β π₯ β βπ¦ β (On β 1o)(πβπ₯):π₯β1-1-ontoβ(Ο βo π¦))) |
23 | | sseq2 3975 |
. . . . . . . . 9
β’ (π₯ = π β (Ο β π₯ β Ο β π)) |
24 | | oveq2 7370 |
. . . . . . . . . . . 12
β’ (π¦ = π€ β (Ο βo π¦) = (Ο βo
π€)) |
25 | 24 | f1oeq3d 6786 |
. . . . . . . . . . 11
β’ (π¦ = π€ β ((πβπ₯):π₯β1-1-ontoβ(Ο βo π¦) β (πβπ₯):π₯β1-1-ontoβ(Ο βo π€))) |
26 | 25 | cbvrexvw 3229 |
. . . . . . . . . 10
β’
(βπ¦ β (On
β 1o)(πβπ₯):π₯β1-1-ontoβ(Ο βo π¦) β βπ€ β (On β 1o)(πβπ₯):π₯β1-1-ontoβ(Ο βo π€)) |
27 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π₯ = π β (πβπ₯) = (πβπ)) |
28 | 27 | f1oeq1d 6784 |
. . . . . . . . . . . 12
β’ (π₯ = π β ((πβπ₯):π₯β1-1-ontoβ(Ο βo π€) β (πβπ):π₯β1-1-ontoβ(Ο βo π€))) |
29 | | f1oeq2 6778 |
. . . . . . . . . . . 12
β’ (π₯ = π β ((πβπ):π₯β1-1-ontoβ(Ο βo π€) β (πβπ):πβ1-1-ontoβ(Ο βo π€))) |
30 | 28, 29 | bitrd 279 |
. . . . . . . . . . 11
β’ (π₯ = π β ((πβπ₯):π₯β1-1-ontoβ(Ο βo π€) β (πβπ):πβ1-1-ontoβ(Ο βo π€))) |
31 | 30 | rexbidv 3176 |
. . . . . . . . . 10
β’ (π₯ = π β (βπ€ β (On β 1o)(πβπ₯):π₯β1-1-ontoβ(Ο βo π€) β βπ€ β (On β 1o)(πβπ):πβ1-1-ontoβ(Ο βo π€))) |
32 | 26, 31 | bitrid 283 |
. . . . . . . . 9
β’ (π₯ = π β (βπ¦ β (On β 1o)(πβπ₯):π₯β1-1-ontoβ(Ο βo π¦) β βπ€ β (On β 1o)(πβπ):πβ1-1-ontoβ(Ο βo π€))) |
33 | 23, 32 | imbi12d 345 |
. . . . . . . 8
β’ (π₯ = π β ((Ο β π₯ β βπ¦ β (On β 1o)(πβπ₯):π₯β1-1-ontoβ(Ο βo π¦)) β (Ο β π β βπ€ β (On β 1o)(πβπ):πβ1-1-ontoβ(Ο βo π€)))) |
34 | 33 | cbvralvw 3228 |
. . . . . . 7
β’
(βπ₯ β
π΄ (Ο β π₯ β βπ¦ β (On β
1o)(πβπ₯):π₯β1-1-ontoβ(Ο βo π¦)) β βπ β π΄ (Ο β π β βπ€ β (On β 1o)(πβπ):πβ1-1-ontoβ(Ο βo π€))) |
35 | 22, 34 | sylib 217 |
. . . . . 6
β’ ((π΄ β On β§ (βπ₯ β π΄ (Ο β π₯ β βπ¦ β (On β 1o)(πβπ₯):π₯β1-1-ontoβ(Ο βo π¦)) β§ π:(Ο βo
2o)β1-1-ontoβΟ)) β βπ β π΄ (Ο β π β βπ€ β (On β 1o)(πβπ):πβ1-1-ontoβ(Ο βo π€))) |
36 | | oveq2 7370 |
. . . . . . . . 9
β’ (π = π§ β (Ο βo π) = (Ο βo
π§)) |
37 | 36 | cbvmptv 5223 |
. . . . . . . 8
β’ (π β (On β
1o) β¦ (Ο βo π)) = (π§ β (On β 1o) β¦
(Ο βo π§)) |
38 | 37 | cnveqi 5835 |
. . . . . . 7
β’ β‘(π β (On β 1o) β¦
(Ο βo π)) = β‘(π§ β (On β 1o) β¦
(Ο βo π§)) |
39 | 38 | fveq1i 6848 |
. . . . . 6
β’ (β‘(π β (On β 1o) β¦
(Ο βo π))βran (πβπ)) = (β‘(π§ β (On β 1o) β¦
(Ο βo π§))βran (πβπ)) |
40 | | 2on 8431 |
. . . . . . . . . 10
β’
2o β On |
41 | | peano1 7830 |
. . . . . . . . . . 11
β’ β
β Ο |
42 | | oen0 8538 |
. . . . . . . . . . 11
β’
(((Ο β On β§ 2o β On) β§ β
β
Ο) β β
β (Ο βo
2o)) |
43 | 41, 42 | mpan2 690 |
. . . . . . . . . 10
β’ ((Ο
β On β§ 2o β On) β β
β (Ο
βo 2o)) |
44 | 4, 40, 43 | mp2an 691 |
. . . . . . . . 9
β’ β
β (Ο βo 2o) |
45 | | eqid 2737 |
. . . . . . . . . 10
β’ (π β (( I βΎ ((Ο
βo 2o) β {β
, (β‘πββ
)})) βͺ {β¨β
,
(β‘πββ
)β©, β¨(β‘πββ
), β
β©})) = (π β (( I βΎ ((Ο
βo 2o) β {β
, (β‘πββ
)})) βͺ {β¨β
,
(β‘πββ
)β©, β¨(β‘πββ
),
β
β©})) |
46 | 45 | fveqf1o 7254 |
. . . . . . . . 9
β’ ((π:(Ο βo
2o)β1-1-ontoβΟ β§ β
β (Ο
βo 2o) β§ β
β Ο) β ((π β (( I βΎ ((Ο
βo 2o) β {β
, (β‘πββ
)})) βͺ {β¨β
,
(β‘πββ
)β©, β¨(β‘πββ
), β
β©})):(Ο
βo 2o)β1-1-ontoβΟ β§ ((π β (( I βΎ ((Ο
βo 2o) β {β
, (β‘πββ
)})) βͺ {β¨β
,
(β‘πββ
)β©, β¨(β‘πββ
),
β
β©}))ββ
) = β
)) |
47 | 44, 41, 46 | mp3an23 1454 |
. . . . . . . 8
β’ (π:(Ο βo
2o)β1-1-ontoβΟ β ((π β (( I βΎ ((Ο
βo 2o) β {β
, (β‘πββ
)})) βͺ {β¨β
,
(β‘πββ
)β©, β¨(β‘πββ
), β
β©})):(Ο
βo 2o)β1-1-ontoβΟ β§ ((π β (( I βΎ ((Ο
βo 2o) β {β
, (β‘πββ
)})) βͺ {β¨β
,
(β‘πββ
)β©, β¨(β‘πββ
),
β
β©}))ββ
) = β
)) |
48 | 47 | ad2antll 728 |
. . . . . . 7
β’ ((π΄ β On β§ (βπ₯ β π΄ (Ο β π₯ β βπ¦ β (On β 1o)(πβπ₯):π₯β1-1-ontoβ(Ο βo π¦)) β§ π:(Ο βo
2o)β1-1-ontoβΟ)) β ((π β (( I βΎ ((Ο
βo 2o) β {β
, (β‘πββ
)})) βͺ {β¨β
,
(β‘πββ
)β©, β¨(β‘πββ
), β
β©})):(Ο
βo 2o)β1-1-ontoβΟ β§ ((π β (( I βΎ ((Ο
βo 2o) β {β
, (β‘πββ
)})) βͺ {β¨β
,
(β‘πββ
)β©, β¨(β‘πββ
),
β
β©}))ββ
) = β
)) |
49 | 48 | simpld 496 |
. . . . . 6
β’ ((π΄ β On β§ (βπ₯ β π΄ (Ο β π₯ β βπ¦ β (On β 1o)(πβπ₯):π₯β1-1-ontoβ(Ο βo π¦)) β§ π:(Ο βo
2o)β1-1-ontoβΟ)) β (π β (( I βΎ ((Ο
βo 2o) β {β
, (β‘πββ
)})) βͺ {β¨β
,
(β‘πββ
)β©, β¨(β‘πββ
), β
β©})):(Ο
βo 2o)β1-1-ontoβΟ) |
50 | 48 | simprd 497 |
. . . . . 6
β’ ((π΄ β On β§ (βπ₯ β π΄ (Ο β π₯ β βπ¦ β (On β 1o)(πβπ₯):π₯β1-1-ontoβ(Ο βo π¦)) β§ π:(Ο βo
2o)β1-1-ontoβΟ)) β ((π β (( I βΎ ((Ο
βo 2o) β {β
, (β‘πββ
)})) βͺ {β¨β
,
(β‘πββ
)β©, β¨(β‘πββ
),
β
β©}))ββ
) = β
) |
51 | 21, 35, 39, 49, 50 | infxpenc2lem3 9964 |
. . . . 5
β’ ((π΄ β On β§ (βπ₯ β π΄ (Ο β π₯ β βπ¦ β (On β 1o)(πβπ₯):π₯β1-1-ontoβ(Ο βo π¦)) β§ π:(Ο βo
2o)β1-1-ontoβΟ)) β βπβπ β π΄ (Ο β π β (πβπ):(π Γ π)β1-1-ontoβπ)) |
52 | 51 | ex 414 |
. . . 4
β’ (π΄ β On β
((βπ₯ β π΄ (Ο β π₯ β βπ¦ β (On β
1o)(πβπ₯):π₯β1-1-ontoβ(Ο βo π¦)) β§ π:(Ο βo
2o)β1-1-ontoβΟ) β βπβπ β π΄ (Ο β π β (πβπ):(π Γ π)β1-1-ontoβπ))) |
53 | 52 | exlimdvv 1938 |
. . 3
β’ (π΄ β On β (βπβπ(βπ₯ β π΄ (Ο β π₯ β βπ¦ β (On β 1o)(πβπ₯):π₯β1-1-ontoβ(Ο βo π¦)) β§ π:(Ο βo
2o)β1-1-ontoβΟ) β βπβπ β π΄ (Ο β π β (πβπ):(π Γ π)β1-1-ontoβπ))) |
54 | 20, 53 | biimtrrid 242 |
. 2
β’ (π΄ β On β ((βπβπ₯ β π΄ (Ο β π₯ β βπ¦ β (On β 1o)(πβπ₯):π₯β1-1-ontoβ(Ο βo π¦)) β§ βπ π:(Ο βo
2o)β1-1-ontoβΟ) β βπβπ β π΄ (Ο β π β (πβπ):(π Γ π)β1-1-ontoβπ))) |
55 | 1, 19, 54 | mp2and 698 |
1
β’ (π΄ β On β βπβπ β π΄ (Ο β π β (πβπ):(π Γ π)β1-1-ontoβπ)) |