Step | Hyp | Ref
| Expression |
1 | | lmbr.2 |
. . 3
β’ (π β π½ β (TopOnβπ)) |
2 | 1 | lmbr 22632 |
. 2
β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§ π β π β§ βπ’ β π½ (π β π’ β βπ§ β ran β€β₯(πΉ βΎ π§):π§βΆπ’)))) |
3 | | uzf 12774 |
. . . . . . . 8
β’
β€β₯:β€βΆπ« β€ |
4 | | ffn 6672 |
. . . . . . . 8
β’
(β€β₯:β€βΆπ« β€ β
β€β₯ Fn β€) |
5 | | reseq2 5936 |
. . . . . . . . . 10
β’ (π§ =
(β€β₯βπ) β (πΉ βΎ π§) = (πΉ βΎ (β€β₯βπ))) |
6 | | id 22 |
. . . . . . . . . 10
β’ (π§ =
(β€β₯βπ) β π§ = (β€β₯βπ)) |
7 | 5, 6 | feq12d 6660 |
. . . . . . . . 9
β’ (π§ =
(β€β₯βπ) β ((πΉ βΎ π§):π§βΆπ’ β (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ’)) |
8 | 7 | rexrn 7041 |
. . . . . . . 8
β’
(β€β₯ Fn β€ β (βπ§ β ran β€β₯(πΉ βΎ π§):π§βΆπ’ β βπ β β€ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ’)) |
9 | 3, 4, 8 | mp2b 10 |
. . . . . . 7
β’
(βπ§ β ran
β€β₯(πΉ
βΎ π§):π§βΆπ’ β βπ β β€ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ’) |
10 | | pmfun 8791 |
. . . . . . . . . . 11
β’ (πΉ β (π βpm β) β Fun
πΉ) |
11 | 10 | ad2antrl 727 |
. . . . . . . . . 10
β’ ((π β§ (πΉ β (π βpm β) β§ π β π)) β Fun πΉ) |
12 | | ffvresb 7076 |
. . . . . . . . . 10
β’ (Fun
πΉ β ((πΉ βΎ
(β€β₯βπ)):(β€β₯βπ)βΆπ’ β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
13 | 11, 12 | syl 17 |
. . . . . . . . 9
β’ ((π β§ (πΉ β (π βpm β) β§ π β π)) β ((πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ’ β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
14 | 13 | rexbidv 3172 |
. . . . . . . 8
β’ ((π β§ (πΉ β (π βpm β) β§ π β π)) β (βπ β β€ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ’ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
15 | | lmbr2.5 |
. . . . . . . . . 10
β’ (π β π β β€) |
16 | 15 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (πΉ β (π βpm β) β§ π β π)) β π β β€) |
17 | | lmbr2.4 |
. . . . . . . . . 10
β’ π =
(β€β₯βπ) |
18 | 17 | rexuz3 15242 |
. . . . . . . . 9
β’ (π β β€ β
(βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’) β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
19 | 16, 18 | syl 17 |
. . . . . . . 8
β’ ((π β§ (πΉ β (π βpm β) β§ π β π)) β (βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’) β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
20 | 14, 19 | bitr4d 282 |
. . . . . . 7
β’ ((π β§ (πΉ β (π βpm β) β§ π β π)) β (βπ β β€ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
21 | 9, 20 | bitrid 283 |
. . . . . 6
β’ ((π β§ (πΉ β (π βpm β) β§ π β π)) β (βπ§ β ran β€β₯(πΉ βΎ π§):π§βΆπ’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
22 | 21 | imbi2d 341 |
. . . . 5
β’ ((π β§ (πΉ β (π βpm β) β§ π β π)) β ((π β π’ β βπ§ β ran β€β₯(πΉ βΎ π§):π§βΆπ’) β (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) |
23 | 22 | ralbidv 3171 |
. . . 4
β’ ((π β§ (πΉ β (π βpm β) β§ π β π)) β (βπ’ β π½ (π β π’ β βπ§ β ran β€β₯(πΉ βΎ π§):π§βΆπ’) β βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) |
24 | 23 | pm5.32da 580 |
. . 3
β’ (π β (((πΉ β (π βpm β) β§ π β π) β§ βπ’ β π½ (π β π’ β βπ§ β ran β€β₯(πΉ βΎ π§):π§βΆπ’)) β ((πΉ β (π βpm β) β§ π β π) β§ βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))))) |
25 | | df-3an 1090 |
. . 3
β’ ((πΉ β (π βpm β) β§ π β π β§ βπ’ β π½ (π β π’ β βπ§ β ran β€β₯(πΉ βΎ π§):π§βΆπ’)) β ((πΉ β (π βpm β) β§ π β π) β§ βπ’ β π½ (π β π’ β βπ§ β ran β€β₯(πΉ βΎ π§):π§βΆπ’))) |
26 | | df-3an 1090 |
. . 3
β’ ((πΉ β (π βpm β) β§ π β π β§ βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) β ((πΉ β (π βpm β) β§ π β π) β§ βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) |
27 | 24, 25, 26 | 3bitr4g 314 |
. 2
β’ (π β ((πΉ β (π βpm β) β§ π β π β§ βπ’ β π½ (π β π’ β βπ§ β ran β€β₯(πΉ βΎ π§):π§βΆπ’)) β (πΉ β (π βpm β) β§ π β π β§ βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))))) |
28 | 2, 27 | bitrd 279 |
1
β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§ π β π β§ βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))))) |