Step | Hyp | Ref
| Expression |
1 | | lmres.2 |
. . . . . . 7
β’ (π β π½ β (TopOnβπ)) |
2 | | toponmax 22428 |
. . . . . . 7
β’ (π½ β (TopOnβπ) β π β π½) |
3 | 1, 2 | syl 17 |
. . . . . 6
β’ (π β π β π½) |
4 | | cnex 11191 |
. . . . . 6
β’ β
β V |
5 | | ssid 4005 |
. . . . . . 7
β’ π β π |
6 | | uzssz 12843 |
. . . . . . . 8
β’
(β€β₯βπ) β β€ |
7 | | zsscn 12566 |
. . . . . . . 8
β’ β€
β β |
8 | 6, 7 | sstri 3992 |
. . . . . . 7
β’
(β€β₯βπ) β β |
9 | | pmss12g 8863 |
. . . . . . 7
β’ (((π β π β§ (β€β₯βπ) β β) β§ (π β π½ β§ β β V)) β (π βpm
(β€β₯βπ)) β (π βpm
β)) |
10 | 5, 8, 9 | mpanl12 701 |
. . . . . 6
β’ ((π β π½ β§ β β V) β (π βpm
(β€β₯βπ)) β (π βpm
β)) |
11 | 3, 4, 10 | sylancl 587 |
. . . . 5
β’ (π β (π βpm
(β€β₯βπ)) β (π βpm
β)) |
12 | | fvex 6905 |
. . . . . 6
β’
(β€β₯βπ) β V |
13 | | lmres.4 |
. . . . . 6
β’ (π β πΉ β (π βpm
β)) |
14 | | pmresg 8864 |
. . . . . 6
β’
(((β€β₯βπ) β V β§ πΉ β (π βpm β)) β (πΉ βΎ
(β€β₯βπ)) β (π βpm
(β€β₯βπ))) |
15 | 12, 13, 14 | sylancr 588 |
. . . . 5
β’ (π β (πΉ βΎ (β€β₯βπ)) β (π βpm
(β€β₯βπ))) |
16 | 11, 15 | sseldd 3984 |
. . . 4
β’ (π β (πΉ βΎ (β€β₯βπ)) β (π βpm
β)) |
17 | 16, 13 | 2thd 265 |
. . 3
β’ (π β ((πΉ βΎ (β€β₯βπ)) β (π βpm β) β πΉ β (π βpm
β))) |
18 | | eqid 2733 |
. . . . . . . . . 10
β’
(β€β₯βπ) = (β€β₯βπ) |
19 | 18 | uztrn2 12841 |
. . . . . . . . 9
β’ ((π β
(β€β₯βπ) β§ π β (β€β₯βπ)) β π β (β€β₯βπ)) |
20 | | dmres 6004 |
. . . . . . . . . . . 12
β’ dom
(πΉ βΎ
(β€β₯βπ)) = ((β€β₯βπ) β© dom πΉ) |
21 | 20 | elin2 4198 |
. . . . . . . . . . 11
β’ (π β dom (πΉ βΎ (β€β₯βπ)) β (π β (β€β₯βπ) β§ π β dom πΉ)) |
22 | 21 | baib 537 |
. . . . . . . . . 10
β’ (π β
(β€β₯βπ) β (π β dom (πΉ βΎ (β€β₯βπ)) β π β dom πΉ)) |
23 | | fvres 6911 |
. . . . . . . . . . 11
β’ (π β
(β€β₯βπ) β ((πΉ βΎ (β€β₯βπ))βπ) = (πΉβπ)) |
24 | 23 | eleq1d 2819 |
. . . . . . . . . 10
β’ (π β
(β€β₯βπ) β (((πΉ βΎ (β€β₯βπ))βπ) β π’ β (πΉβπ) β π’)) |
25 | 22, 24 | anbi12d 632 |
. . . . . . . . 9
β’ (π β
(β€β₯βπ) β ((π β dom (πΉ βΎ (β€β₯βπ)) β§ ((πΉ βΎ (β€β₯βπ))βπ) β π’) β (π β dom πΉ β§ (πΉβπ) β π’))) |
26 | 19, 25 | syl 17 |
. . . . . . . 8
β’ ((π β
(β€β₯βπ) β§ π β (β€β₯βπ)) β ((π β dom (πΉ βΎ (β€β₯βπ)) β§ ((πΉ βΎ (β€β₯βπ))βπ) β π’) β (π β dom πΉ β§ (πΉβπ) β π’))) |
27 | 26 | ralbidva 3176 |
. . . . . . 7
β’ (π β
(β€β₯βπ) β (βπ β (β€β₯βπ)(π β dom (πΉ βΎ (β€β₯βπ)) β§ ((πΉ βΎ (β€β₯βπ))βπ) β π’) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
28 | 27 | rexbiia 3093 |
. . . . . 6
β’
(βπ β
(β€β₯βπ)βπ β (β€β₯βπ)(π β dom (πΉ βΎ (β€β₯βπ)) β§ ((πΉ βΎ (β€β₯βπ))βπ) β π’) β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)) |
29 | 28 | imbi2i 336 |
. . . . 5
β’ ((π β π’ β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β dom (πΉ βΎ (β€β₯βπ)) β§ ((πΉ βΎ (β€β₯βπ))βπ) β π’)) β (π β π’ β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
30 | 29 | ralbii 3094 |
. . . 4
β’
(βπ’ β
π½ (π β π’ β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β dom (πΉ βΎ (β€β₯βπ)) β§ ((πΉ βΎ (β€β₯βπ))βπ) β π’)) β βπ’ β π½ (π β π’ β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
31 | 30 | a1i 11 |
. . 3
β’ (π β (βπ’ β π½ (π β π’ β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β dom (πΉ βΎ (β€β₯βπ)) β§ ((πΉ βΎ (β€β₯βπ))βπ) β π’)) β βπ’ β π½ (π β π’ β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) |
32 | 17, 31 | 3anbi13d 1439 |
. 2
β’ (π β (((πΉ βΎ (β€β₯βπ)) β (π βpm β) β§ π β π β§ βπ’ β π½ (π β π’ β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β dom (πΉ βΎ (β€β₯βπ)) β§ ((πΉ βΎ (β€β₯βπ))βπ) β π’))) β (πΉ β (π βpm β) β§ π β π β§ βπ’ β π½ (π β π’ β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))))) |
33 | | lmres.5 |
. . 3
β’ (π β π β β€) |
34 | 1, 18, 33 | lmbr2 22763 |
. 2
β’ (π β ((πΉ βΎ (β€β₯βπ))(βπ‘βπ½)π β ((πΉ βΎ (β€β₯βπ)) β (π βpm β) β§ π β π β§ βπ’ β π½ (π β π’ β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β dom (πΉ βΎ (β€β₯βπ)) β§ ((πΉ βΎ (β€β₯βπ))βπ) β π’))))) |
35 | 1, 18, 33 | lmbr2 22763 |
. 2
β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§ π β π β§ βπ’ β π½ (π β π’ β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))))) |
36 | 32, 34, 35 | 3bitr4rd 312 |
1
β’ (π β (πΉ(βπ‘βπ½)π β (πΉ βΎ (β€β₯βπ))(βπ‘βπ½)π)) |