Step | Hyp | Ref
| Expression |
1 | | lmres.2 |
. . . . . . 7
β’ (π β π½ β (TopOnβπ)) |
2 | | toponmax 13495 |
. . . . . . 7
β’ (π½ β (TopOnβπ) β π β π½) |
3 | 1, 2 | syl 14 |
. . . . . 6
β’ (π β π β π½) |
4 | | cnex 7934 |
. . . . . 6
β’ β
β V |
5 | | ssid 3175 |
. . . . . . 7
β’ π β π |
6 | | uzssz 9546 |
. . . . . . . 8
β’
(β€β₯βπ) β β€ |
7 | | zsscn 9260 |
. . . . . . . 8
β’ β€
β β |
8 | 6, 7 | sstri 3164 |
. . . . . . 7
β’
(β€β₯βπ) β β |
9 | | pmss12g 6674 |
. . . . . . 7
β’ (((π β π β§ (β€β₯βπ) β β) β§ (π β π½ β§ β β V)) β (π βpm
(β€β₯βπ)) β (π βpm
β)) |
10 | 5, 8, 9 | mpanl12 436 |
. . . . . 6
β’ ((π β π½ β§ β β V) β (π βpm
(β€β₯βπ)) β (π βpm
β)) |
11 | 3, 4, 10 | sylancl 413 |
. . . . 5
β’ (π β (π βpm
(β€β₯βπ)) β (π βpm
β)) |
12 | | zex 9261 |
. . . . . . 7
β’ β€
β V |
13 | 12, 6 | ssexi 4141 |
. . . . . 6
β’
(β€β₯βπ) β V |
14 | | lmres.4 |
. . . . . 6
β’ (π β πΉ β (π βpm
β)) |
15 | | pmresg 6675 |
. . . . . 6
β’
(((β€β₯βπ) β V β§ πΉ β (π βpm β)) β
(πΉ βΎ
(β€β₯βπ)) β (π βpm
(β€β₯βπ))) |
16 | 13, 14, 15 | sylancr 414 |
. . . . 5
β’ (π β (πΉ βΎ (β€β₯βπ)) β (π βpm
(β€β₯βπ))) |
17 | 11, 16 | sseldd 3156 |
. . . 4
β’ (π β (πΉ βΎ (β€β₯βπ)) β (π βpm
β)) |
18 | 17, 14 | 2thd 175 |
. . 3
β’ (π β ((πΉ βΎ (β€β₯βπ)) β (π βpm β) β
πΉ β (π βpm
β))) |
19 | | eqid 2177 |
. . . . . . . . . 10
β’
(β€β₯βπ) = (β€β₯βπ) |
20 | 19 | uztrn2 9544 |
. . . . . . . . 9
β’ ((π β
(β€β₯βπ) β§ π β (β€β₯βπ)) β π β (β€β₯βπ)) |
21 | | dmres 4928 |
. . . . . . . . . . . 12
β’ dom
(πΉ βΎ
(β€β₯βπ)) = ((β€β₯βπ) β© dom πΉ) |
22 | 21 | elin2 3323 |
. . . . . . . . . . 11
β’ (π β dom (πΉ βΎ (β€β₯βπ)) β (π β (β€β₯βπ) β§ π β dom πΉ)) |
23 | 22 | baib 919 |
. . . . . . . . . 10
β’ (π β
(β€β₯βπ) β (π β dom (πΉ βΎ (β€β₯βπ)) β π β dom πΉ)) |
24 | | fvres 5539 |
. . . . . . . . . . 11
β’ (π β
(β€β₯βπ) β ((πΉ βΎ (β€β₯βπ))βπ) = (πΉβπ)) |
25 | 24 | eleq1d 2246 |
. . . . . . . . . 10
β’ (π β
(β€β₯βπ) β (((πΉ βΎ (β€β₯βπ))βπ) β π’ β (πΉβπ) β π’)) |
26 | 23, 25 | anbi12d 473 |
. . . . . . . . 9
β’ (π β
(β€β₯βπ) β ((π β dom (πΉ βΎ (β€β₯βπ)) β§ ((πΉ βΎ (β€β₯βπ))βπ) β π’) β (π β dom πΉ β§ (πΉβπ) β π’))) |
27 | 20, 26 | syl 14 |
. . . . . . . 8
β’ ((π β
(β€β₯βπ) β§ π β (β€β₯βπ)) β ((π β dom (πΉ βΎ (β€β₯βπ)) β§ ((πΉ βΎ (β€β₯βπ))βπ) β π’) β (π β dom πΉ β§ (πΉβπ) β π’))) |
28 | 27 | ralbidva 2473 |
. . . . . . 7
β’ (π β
(β€β₯βπ) β (βπ β (β€β₯βπ)(π β dom (πΉ βΎ (β€β₯βπ)) β§ ((πΉ βΎ (β€β₯βπ))βπ) β π’) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
29 | 28 | rexbiia 2492 |
. . . . . 6
β’
(βπ β
(β€β₯βπ)βπ β (β€β₯βπ)(π β dom (πΉ βΎ (β€β₯βπ)) β§ ((πΉ βΎ (β€β₯βπ))βπ) β π’) β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)) |
30 | 29 | imbi2i 226 |
. . . . 5
β’ ((π β π’ β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β dom (πΉ βΎ (β€β₯βπ)) β§ ((πΉ βΎ (β€β₯βπ))βπ) β π’)) β (π β π’ β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
31 | 30 | ralbii 2483 |
. . . 4
β’
(βπ’ β
π½ (π β π’ β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β dom (πΉ βΎ (β€β₯βπ)) β§ ((πΉ βΎ (β€β₯βπ))βπ) β π’)) β βπ’ β π½ (π β π’ β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
32 | 31 | a1i 9 |
. . 3
β’ (π β (βπ’ β π½ (π β π’ β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β dom (πΉ βΎ (β€β₯βπ)) β§ ((πΉ βΎ (β€β₯βπ))βπ) β π’)) β βπ’ β π½ (π β π’ β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) |
33 | 18, 32 | 3anbi13d 1314 |
. 2
β’ (π β (((πΉ βΎ (β€β₯βπ)) β (π βpm β) β§
π β π β§ βπ’ β π½ (π β π’ β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β dom (πΉ βΎ (β€β₯βπ)) β§ ((πΉ βΎ (β€β₯βπ))βπ) β π’))) β (πΉ β (π βpm β) β§
π β π β§ βπ’ β π½ (π β π’ β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))))) |
34 | | lmres.5 |
. . 3
β’ (π β π β β€) |
35 | 1, 19, 34 | lmbr2 13684 |
. 2
β’ (π β ((πΉ βΎ (β€β₯βπ))(βπ‘βπ½)π β ((πΉ βΎ (β€β₯βπ)) β (π βpm β) β§
π β π β§ βπ’ β π½ (π β π’ β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β dom (πΉ βΎ (β€β₯βπ)) β§ ((πΉ βΎ (β€β₯βπ))βπ) β π’))))) |
36 | 1, 19, 34 | lmbr2 13684 |
. 2
β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§
π β π β§ βπ’ β π½ (π β π’ β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))))) |
37 | 33, 35, 36 | 3bitr4rd 221 |
1
β’ (π β (πΉ(βπ‘βπ½)π β (πΉ βΎ (β€β₯βπ))(βπ‘βπ½)π)) |