Step | Hyp | Ref
| Expression |
1 | | lmbr.2 |
. . 3
β’ (π β π½ β (TopOnβπ)) |
2 | | lmbr2.4 |
. . 3
β’ π =
(β€β₯βπ) |
3 | | lmbr2.5 |
. . 3
β’ (π β π β β€) |
4 | 1, 2, 3 | lmbr2 22763 |
. 2
β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§ π β π β§ βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))))) |
5 | | 3anass 1096 |
. . 3
β’ ((πΉ β (π βpm β) β§ π β π β§ βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) β (πΉ β (π βpm β) β§ (π β π β§ βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))))) |
6 | 2 | uztrn2 12841 |
. . . . . . . . . . 11
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
7 | | lmbrf.7 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β (πΉβπ) = π΄) |
8 | 7 | eleq1d 2819 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β ((πΉβπ) β π’ β π΄ β π’)) |
9 | | lmbrf.6 |
. . . . . . . . . . . . . . . 16
β’ (π β πΉ:πβΆπ) |
10 | 9 | fdmd 6729 |
. . . . . . . . . . . . . . 15
β’ (π β dom πΉ = π) |
11 | 10 | eleq2d 2820 |
. . . . . . . . . . . . . 14
β’ (π β (π β dom πΉ β π β π)) |
12 | 11 | biimpar 479 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β π β dom πΉ) |
13 | 12 | biantrurd 534 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β ((πΉβπ) β π’ β (π β dom πΉ β§ (πΉβπ) β π’))) |
14 | 8, 13 | bitr3d 281 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (π΄ β π’ β (π β dom πΉ β§ (πΉβπ) β π’))) |
15 | 6, 14 | sylan2 594 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ π β (β€β₯βπ))) β (π΄ β π’ β (π β dom πΉ β§ (πΉβπ) β π’))) |
16 | 15 | anassrs 469 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (π΄ β π’ β (π β dom πΉ β§ (πΉβπ) β π’))) |
17 | 16 | ralbidva 3176 |
. . . . . . . 8
β’ ((π β§ π β π) β (βπ β (β€β₯βπ)π΄ β π’ β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
18 | 17 | rexbidva 3177 |
. . . . . . 7
β’ (π β (βπ β π βπ β (β€β₯βπ)π΄ β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
19 | 18 | imbi2d 341 |
. . . . . 6
β’ (π β ((π β π’ β βπ β π βπ β (β€β₯βπ)π΄ β π’) β (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) |
20 | 19 | ralbidv 3178 |
. . . . 5
β’ (π β (βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)π΄ β π’) β βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) |
21 | 20 | anbi2d 630 |
. . . 4
β’ (π β ((π β π β§ βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)π΄ β π’)) β (π β π β§ βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))))) |
22 | | toponmax 22428 |
. . . . . . . 8
β’ (π½ β (TopOnβπ) β π β π½) |
23 | 1, 22 | syl 17 |
. . . . . . 7
β’ (π β π β π½) |
24 | | cnex 11191 |
. . . . . . 7
β’ β
β V |
25 | 23, 24 | jctir 522 |
. . . . . 6
β’ (π β (π β π½ β§ β β V)) |
26 | | uzssz 12843 |
. . . . . . . . 9
β’
(β€β₯βπ) β β€ |
27 | | zsscn 12566 |
. . . . . . . . 9
β’ β€
β β |
28 | 26, 27 | sstri 3992 |
. . . . . . . 8
β’
(β€β₯βπ) β β |
29 | 2, 28 | eqsstri 4017 |
. . . . . . 7
β’ π β
β |
30 | 9, 29 | jctir 522 |
. . . . . 6
β’ (π β (πΉ:πβΆπ β§ π β β)) |
31 | | elpm2r 8839 |
. . . . . 6
β’ (((π β π½ β§ β β V) β§ (πΉ:πβΆπ β§ π β β)) β πΉ β (π βpm
β)) |
32 | 25, 30, 31 | syl2anc 585 |
. . . . 5
β’ (π β πΉ β (π βpm
β)) |
33 | 32 | biantrurd 534 |
. . . 4
β’ (π β ((π β π β§ βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) β (πΉ β (π βpm β) β§ (π β π β§ βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))))) |
34 | 21, 33 | bitr2d 280 |
. . 3
β’ (π β ((πΉ β (π βpm β) β§ (π β π β§ βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) β (π β π β§ βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)π΄ β π’)))) |
35 | 5, 34 | bitrid 283 |
. 2
β’ (π β ((πΉ β (π βpm β) β§ π β π β§ βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) β (π β π β§ βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)π΄ β π’)))) |
36 | 4, 35 | bitrd 279 |
1
β’ (π β (πΉ(βπ‘βπ½)π β (π β π β§ βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)π΄ β π’)))) |