Step | Hyp | Ref
| Expression |
1 | | lmff.5 |
. . . . . 6
β’ (π β πΉ β dom
(βπ‘βπ½)) |
2 | | eldm2g 5859 |
. . . . . . 7
β’ (πΉ β dom
(βπ‘βπ½) β (πΉ β dom
(βπ‘βπ½) β βπ¦β¨πΉ, π¦β© β
(βπ‘βπ½))) |
3 | 2 | ibi 267 |
. . . . . 6
β’ (πΉ β dom
(βπ‘βπ½) β βπ¦β¨πΉ, π¦β© β
(βπ‘βπ½)) |
4 | 1, 3 | syl 17 |
. . . . 5
β’ (π β βπ¦β¨πΉ, π¦β© β
(βπ‘βπ½)) |
5 | | df-br 5110 |
. . . . . 6
β’ (πΉ(βπ‘βπ½)π¦ β β¨πΉ, π¦β© β
(βπ‘βπ½)) |
6 | 5 | exbii 1851 |
. . . . 5
β’
(βπ¦ πΉ(βπ‘βπ½)π¦ β βπ¦β¨πΉ, π¦β© β
(βπ‘βπ½)) |
7 | 4, 6 | sylibr 233 |
. . . 4
β’ (π β βπ¦ πΉ(βπ‘βπ½)π¦) |
8 | | lmff.3 |
. . . . . 6
β’ (π β π½ β (TopOnβπ)) |
9 | | lmcl 22671 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΉ(βπ‘βπ½)π¦) β π¦ β π) |
10 | 8, 9 | sylan 581 |
. . . . 5
β’ ((π β§ πΉ(βπ‘βπ½)π¦) β π¦ β π) |
11 | | eleq2 2823 |
. . . . . . 7
β’ (π = π β (π¦ β π β π¦ β π)) |
12 | | feq3 6655 |
. . . . . . . 8
β’ (π = π β ((πΉ βΎ π₯):π₯βΆπ β (πΉ βΎ π₯):π₯βΆπ)) |
13 | 12 | rexbidv 3172 |
. . . . . . 7
β’ (π = π β (βπ₯ β ran β€β₯(πΉ βΎ π₯):π₯βΆπ β βπ₯ β ran β€β₯(πΉ βΎ π₯):π₯βΆπ)) |
14 | 11, 13 | imbi12d 345 |
. . . . . 6
β’ (π = π β ((π¦ β π β βπ₯ β ran β€β₯(πΉ βΎ π₯):π₯βΆπ) β (π¦ β π β βπ₯ β ran β€β₯(πΉ βΎ π₯):π₯βΆπ))) |
15 | 8 | lmbr 22632 |
. . . . . . . 8
β’ (π β (πΉ(βπ‘βπ½)π¦ β (πΉ β (π βpm β) β§ π¦ β π β§ βπ β π½ (π¦ β π β βπ₯ β ran β€β₯(πΉ βΎ π₯):π₯βΆπ)))) |
16 | 15 | biimpa 478 |
. . . . . . 7
β’ ((π β§ πΉ(βπ‘βπ½)π¦) β (πΉ β (π βpm β) β§ π¦ β π β§ βπ β π½ (π¦ β π β βπ₯ β ran β€β₯(πΉ βΎ π₯):π₯βΆπ))) |
17 | 16 | simp3d 1145 |
. . . . . 6
β’ ((π β§ πΉ(βπ‘βπ½)π¦) β βπ β π½ (π¦ β π β βπ₯ β ran β€β₯(πΉ βΎ π₯):π₯βΆπ)) |
18 | | toponmax 22298 |
. . . . . . . 8
β’ (π½ β (TopOnβπ) β π β π½) |
19 | 8, 18 | syl 17 |
. . . . . . 7
β’ (π β π β π½) |
20 | 19 | adantr 482 |
. . . . . 6
β’ ((π β§ πΉ(βπ‘βπ½)π¦) β π β π½) |
21 | 14, 17, 20 | rspcdva 3584 |
. . . . 5
β’ ((π β§ πΉ(βπ‘βπ½)π¦) β (π¦ β π β βπ₯ β ran β€β₯(πΉ βΎ π₯):π₯βΆπ)) |
22 | 10, 21 | mpd 15 |
. . . 4
β’ ((π β§ πΉ(βπ‘βπ½)π¦) β βπ₯ β ran β€β₯(πΉ βΎ π₯):π₯βΆπ) |
23 | 7, 22 | exlimddv 1939 |
. . 3
β’ (π β βπ₯ β ran β€β₯(πΉ βΎ π₯):π₯βΆπ) |
24 | | uzf 12774 |
. . . 4
β’
β€β₯:β€βΆπ« β€ |
25 | | ffn 6672 |
. . . 4
β’
(β€β₯:β€βΆπ« β€ β
β€β₯ Fn β€) |
26 | | reseq2 5936 |
. . . . . 6
β’ (π₯ =
(β€β₯βπ) β (πΉ βΎ π₯) = (πΉ βΎ (β€β₯βπ))) |
27 | | id 22 |
. . . . . 6
β’ (π₯ =
(β€β₯βπ) β π₯ = (β€β₯βπ)) |
28 | 26, 27 | feq12d 6660 |
. . . . 5
β’ (π₯ =
(β€β₯βπ) β ((πΉ βΎ π₯):π₯βΆπ β (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ)) |
29 | 28 | rexrn 7041 |
. . . 4
β’
(β€β₯ Fn β€ β (βπ₯ β ran β€β₯(πΉ βΎ π₯):π₯βΆπ β βπ β β€ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ)) |
30 | 24, 25, 29 | mp2b 10 |
. . 3
β’
(βπ₯ β ran
β€β₯(πΉ
βΎ π₯):π₯βΆπ β βπ β β€ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ) |
31 | 23, 30 | sylib 217 |
. 2
β’ (π β βπ β β€ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ) |
32 | | lmff.4 |
. . . 4
β’ (π β π β β€) |
33 | | lmff.1 |
. . . . 5
β’ π =
(β€β₯βπ) |
34 | 33 | rexuz3 15242 |
. . . 4
β’ (π β β€ β
(βπ β π βπ₯ β (β€β₯βπ)(π₯ β dom πΉ β§ (πΉβπ₯) β π) β βπ β β€ βπ₯ β (β€β₯βπ)(π₯ β dom πΉ β§ (πΉβπ₯) β π))) |
35 | 32, 34 | syl 17 |
. . 3
β’ (π β (βπ β π βπ₯ β (β€β₯βπ)(π₯ β dom πΉ β§ (πΉβπ₯) β π) β βπ β β€ βπ₯ β (β€β₯βπ)(π₯ β dom πΉ β§ (πΉβπ₯) β π))) |
36 | 16 | simp1d 1143 |
. . . . . . 7
β’ ((π β§ πΉ(βπ‘βπ½)π¦) β πΉ β (π βpm
β)) |
37 | 7, 36 | exlimddv 1939 |
. . . . . 6
β’ (π β πΉ β (π βpm
β)) |
38 | | pmfun 8791 |
. . . . . 6
β’ (πΉ β (π βpm β) β Fun
πΉ) |
39 | 37, 38 | syl 17 |
. . . . 5
β’ (π β Fun πΉ) |
40 | | ffvresb 7076 |
. . . . 5
β’ (Fun
πΉ β ((πΉ βΎ
(β€β₯βπ)):(β€β₯βπ)βΆπ β βπ₯ β (β€β₯βπ)(π₯ β dom πΉ β§ (πΉβπ₯) β π))) |
41 | 39, 40 | syl 17 |
. . . 4
β’ (π β ((πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ β βπ₯ β (β€β₯βπ)(π₯ β dom πΉ β§ (πΉβπ₯) β π))) |
42 | 41 | rexbidv 3172 |
. . 3
β’ (π β (βπ β π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ β βπ β π βπ₯ β (β€β₯βπ)(π₯ β dom πΉ β§ (πΉβπ₯) β π))) |
43 | 41 | rexbidv 3172 |
. . 3
β’ (π β (βπ β β€ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ β βπ β β€ βπ₯ β (β€β₯βπ)(π₯ β dom πΉ β§ (πΉβπ₯) β π))) |
44 | 35, 42, 43 | 3bitr4d 311 |
. 2
β’ (π β (βπ β π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ β βπ β β€ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ)) |
45 | 31, 44 | mpbird 257 |
1
β’ (π β βπ β π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ) |