Step | Hyp | Ref
| Expression |
1 | | infxpenc2.2 |
. . . 4
β’ (π β βπ β π΄ (Ο β π β βπ€ β (On β 1o)(πβπ):πβ1-1-ontoβ(Ο βo π€))) |
2 | 1 | r19.21bi 3237 |
. . 3
β’ ((π β§ π β π΄) β (Ο β π β βπ€ β (On β 1o)(πβπ):πβ1-1-ontoβ(Ο βo π€))) |
3 | 2 | impr 456 |
. 2
β’ ((π β§ (π β π΄ β§ Ο β π)) β βπ€ β (On β 1o)(πβπ):πβ1-1-ontoβ(Ο βo π€)) |
4 | | simpr 486 |
. . 3
β’ (((π β§ (π β π΄ β§ Ο β π)) β§ (π€ β (On β 1o) β§
(πβπ):πβ1-1-ontoβ(Ο βo π€))) β (π€ β (On β 1o) β§
(πβπ):πβ1-1-ontoβ(Ο βo π€))) |
5 | | infxpenc2.3 |
. . . . . 6
β’ π = (β‘(π₯ β (On β 1o) β¦
(Ο βo π₯))βran (πβπ)) |
6 | | oveq2 7370 |
. . . . . . . . . 10
β’ (π₯ = π€ β (Ο βo π₯) = (Ο βo
π€)) |
7 | | eqid 2737 |
. . . . . . . . . 10
β’ (π₯ β (On β
1o) β¦ (Ο βo π₯)) = (π₯ β (On β 1o) β¦
(Ο βo π₯)) |
8 | | ovex 7395 |
. . . . . . . . . 10
β’ (Ο
βo π€)
β V |
9 | 6, 7, 8 | fvmpt 6953 |
. . . . . . . . 9
β’ (π€ β (On β
1o) β ((π₯
β (On β 1o) β¦ (Ο βo π₯))βπ€) = (Ο βo π€)) |
10 | 9 | ad2antrl 727 |
. . . . . . . 8
β’ (((π β§ (π β π΄ β§ Ο β π)) β§ (π€ β (On β 1o) β§
(πβπ):πβ1-1-ontoβ(Ο βo π€))) β ((π₯ β (On β 1o) β¦
(Ο βo π₯))βπ€) = (Ο βo π€)) |
11 | | f1ofo 6796 |
. . . . . . . . . 10
β’ ((πβπ):πβ1-1-ontoβ(Ο βo π€) β (πβπ):πβontoβ(Ο βo π€)) |
12 | 11 | ad2antll 728 |
. . . . . . . . 9
β’ (((π β§ (π β π΄ β§ Ο β π)) β§ (π€ β (On β 1o) β§
(πβπ):πβ1-1-ontoβ(Ο βo π€))) β (πβπ):πβontoβ(Ο βo π€)) |
13 | | forn 6764 |
. . . . . . . . 9
β’ ((πβπ):πβontoβ(Ο βo π€) β ran (πβπ) = (Ο βo π€)) |
14 | 12, 13 | syl 17 |
. . . . . . . 8
β’ (((π β§ (π β π΄ β§ Ο β π)) β§ (π€ β (On β 1o) β§
(πβπ):πβ1-1-ontoβ(Ο βo π€))) β ran (πβπ) = (Ο βo π€)) |
15 | 10, 14 | eqtr4d 2780 |
. . . . . . 7
β’ (((π β§ (π β π΄ β§ Ο β π)) β§ (π€ β (On β 1o) β§
(πβπ):πβ1-1-ontoβ(Ο βo π€))) β ((π₯ β (On β 1o) β¦
(Ο βo π₯))βπ€) = ran (πβπ)) |
16 | | ovex 7395 |
. . . . . . . . . . 11
β’ (Ο
βo π₯)
β V |
17 | 16 | 2a1i 12 |
. . . . . . . . . 10
β’ (((π β§ (π β π΄ β§ Ο β π)) β§ (π€ β (On β 1o) β§
(πβπ):πβ1-1-ontoβ(Ο βo π€))) β (π₯ β (On β 1o) β
(Ο βo π₯) β V)) |
18 | | omelon 9589 |
. . . . . . . . . . . . 13
β’ Ο
β On |
19 | | 1onn 8591 |
. . . . . . . . . . . . 13
β’
1o β Ο |
20 | | ondif2 8453 |
. . . . . . . . . . . . 13
β’ (Ο
β (On β 2o) β (Ο β On β§ 1o
β Ο)) |
21 | 18, 19, 20 | mpbir2an 710 |
. . . . . . . . . . . 12
β’ Ο
β (On β 2o) |
22 | | eldifi 4091 |
. . . . . . . . . . . . 13
β’ (π₯ β (On β
1o) β π₯
β On) |
23 | 22 | ad2antrl 727 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β π΄ β§ Ο β π)) β§ (π€ β (On β 1o) β§
(πβπ):πβ1-1-ontoβ(Ο βo π€))) β§ (π₯ β (On β 1o) β§
π¦ β (On β
1o))) β π₯
β On) |
24 | | eldifi 4091 |
. . . . . . . . . . . . 13
β’ (π¦ β (On β
1o) β π¦
β On) |
25 | 24 | ad2antll 728 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β π΄ β§ Ο β π)) β§ (π€ β (On β 1o) β§
(πβπ):πβ1-1-ontoβ(Ο βo π€))) β§ (π₯ β (On β 1o) β§
π¦ β (On β
1o))) β π¦
β On) |
26 | | oecan 8541 |
. . . . . . . . . . . 12
β’ ((Ο
β (On β 2o) β§ π₯ β On β§ π¦ β On) β ((Ο
βo π₯) =
(Ο βo π¦) β π₯ = π¦)) |
27 | 21, 23, 25, 26 | mp3an2i 1467 |
. . . . . . . . . . 11
β’ ((((π β§ (π β π΄ β§ Ο β π)) β§ (π€ β (On β 1o) β§
(πβπ):πβ1-1-ontoβ(Ο βo π€))) β§ (π₯ β (On β 1o) β§
π¦ β (On β
1o))) β ((Ο βo π₯) = (Ο βo π¦) β π₯ = π¦)) |
28 | 27 | ex 414 |
. . . . . . . . . 10
β’ (((π β§ (π β π΄ β§ Ο β π)) β§ (π€ β (On β 1o) β§
(πβπ):πβ1-1-ontoβ(Ο βo π€))) β ((π₯ β (On β 1o) β§
π¦ β (On β
1o)) β ((Ο βo π₯) = (Ο βo π¦) β π₯ = π¦))) |
29 | 17, 28 | dom2lem 8939 |
. . . . . . . . 9
β’ (((π β§ (π β π΄ β§ Ο β π)) β§ (π€ β (On β 1o) β§
(πβπ):πβ1-1-ontoβ(Ο βo π€))) β (π₯ β (On β 1o) β¦
(Ο βo π₯)):(On β 1o)β1-1βV) |
30 | | f1f1orn 6800 |
. . . . . . . . 9
β’ ((π₯ β (On β
1o) β¦ (Ο βo π₯)):(On β 1o)β1-1βV β (π₯ β (On β 1o) β¦
(Ο βo π₯)):(On β 1o)β1-1-ontoβran (π₯ β (On β 1o) β¦
(Ο βo π₯))) |
31 | 29, 30 | syl 17 |
. . . . . . . 8
β’ (((π β§ (π β π΄ β§ Ο β π)) β§ (π€ β (On β 1o) β§
(πβπ):πβ1-1-ontoβ(Ο βo π€))) β (π₯ β (On β 1o) β¦
(Ο βo π₯)):(On β 1o)β1-1-ontoβran (π₯ β (On β 1o) β¦
(Ο βo π₯))) |
32 | | simprl 770 |
. . . . . . . 8
β’ (((π β§ (π β π΄ β§ Ο β π)) β§ (π€ β (On β 1o) β§
(πβπ):πβ1-1-ontoβ(Ο βo π€))) β π€ β (On β
1o)) |
33 | | f1ocnvfv 7229 |
. . . . . . . 8
β’ (((π₯ β (On β
1o) β¦ (Ο βo π₯)):(On β 1o)β1-1-ontoβran (π₯ β (On β 1o) β¦
(Ο βo π₯)) β§ π€ β (On β 1o)) β
(((π₯ β (On β
1o) β¦ (Ο βo π₯))βπ€) = ran (πβπ) β (β‘(π₯ β (On β 1o) β¦
(Ο βo π₯))βran (πβπ)) = π€)) |
34 | 31, 32, 33 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ (π β π΄ β§ Ο β π)) β§ (π€ β (On β 1o) β§
(πβπ):πβ1-1-ontoβ(Ο βo π€))) β (((π₯ β (On β 1o) β¦
(Ο βo π₯))βπ€) = ran (πβπ) β (β‘(π₯ β (On β 1o) β¦
(Ο βo π₯))βran (πβπ)) = π€)) |
35 | 15, 34 | mpd 15 |
. . . . . 6
β’ (((π β§ (π β π΄ β§ Ο β π)) β§ (π€ β (On β 1o) β§
(πβπ):πβ1-1-ontoβ(Ο βo π€))) β (β‘(π₯ β (On β 1o) β¦
(Ο βo π₯))βran (πβπ)) = π€) |
36 | 5, 35 | eqtrid 2789 |
. . . . 5
β’ (((π β§ (π β π΄ β§ Ο β π)) β§ (π€ β (On β 1o) β§
(πβπ):πβ1-1-ontoβ(Ο βo π€))) β π = π€) |
37 | 36 | eleq1d 2823 |
. . . 4
β’ (((π β§ (π β π΄ β§ Ο β π)) β§ (π€ β (On β 1o) β§
(πβπ):πβ1-1-ontoβ(Ο βo π€))) β (π β (On β 1o) β
π€ β (On β
1o))) |
38 | 36 | oveq2d 7378 |
. . . . 5
β’ (((π β§ (π β π΄ β§ Ο β π)) β§ (π€ β (On β 1o) β§
(πβπ):πβ1-1-ontoβ(Ο βo π€))) β (Ο βo π) = (Ο βo
π€)) |
39 | 38 | f1oeq3d 6786 |
. . . 4
β’ (((π β§ (π β π΄ β§ Ο β π)) β§ (π€ β (On β 1o) β§
(πβπ):πβ1-1-ontoβ(Ο βo π€))) β ((πβπ):πβ1-1-ontoβ(Ο βo π) β (πβπ):πβ1-1-ontoβ(Ο βo π€))) |
40 | 37, 39 | anbi12d 632 |
. . 3
β’ (((π β§ (π β π΄ β§ Ο β π)) β§ (π€ β (On β 1o) β§
(πβπ):πβ1-1-ontoβ(Ο βo π€))) β ((π β (On β 1o) β§
(πβπ):πβ1-1-ontoβ(Ο βo π)) β (π€ β (On β 1o) β§
(πβπ):πβ1-1-ontoβ(Ο βo π€)))) |
41 | 4, 40 | mpbird 257 |
. 2
β’ (((π β§ (π β π΄ β§ Ο β π)) β§ (π€ β (On β 1o) β§
(πβπ):πβ1-1-ontoβ(Ο βo π€))) β (π β (On β 1o) β§
(πβπ):πβ1-1-ontoβ(Ο βo π))) |
42 | 3, 41 | rexlimddv 3159 |
1
β’ ((π β§ (π β π΄ β§ Ο β π)) β (π β (On β 1o) β§
(πβπ):πβ1-1-ontoβ(Ο βo π))) |