Step | Hyp | Ref
| Expression |
1 | | lmbr3.2 |
. . 3
β’ (π β π½ β (TopOnβπ)) |
2 | 1 | lmbr3v 44072 |
. 2
β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§ π β π β§ βπ£ β π½ (π β π£ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π£))))) |
3 | | eleq2w 2818 |
. . . . 5
β’ (π£ = π’ β (π β π£ β π β π’)) |
4 | | eleq2w 2818 |
. . . . . . . 8
β’ (π£ = π’ β ((πΉβπ) β π£ β (πΉβπ) β π’)) |
5 | 4 | anbi2d 630 |
. . . . . . 7
β’ (π£ = π’ β ((π β dom πΉ β§ (πΉβπ) β π£) β (π β dom πΉ β§ (πΉβπ) β π’))) |
6 | 5 | rexralbidv 3211 |
. . . . . 6
β’ (π£ = π’ β (βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π£) β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
7 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = π β (β€β₯βπ) =
(β€β₯βπ)) |
8 | 7 | raleqdv 3312 |
. . . . . . . 8
β’ (π = π β (βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
9 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²ππ |
10 | | lmbr3.1 |
. . . . . . . . . . . 12
β’
β²ππΉ |
11 | 10 | nfdm 5907 |
. . . . . . . . . . 11
β’
β²πdom
πΉ |
12 | 9, 11 | nfel 2918 |
. . . . . . . . . 10
β’
β²π π β dom πΉ |
13 | 10, 9 | nffv 6853 |
. . . . . . . . . . 11
β’
β²π(πΉβπ) |
14 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²ππ’ |
15 | 13, 14 | nfel 2918 |
. . . . . . . . . 10
β’
β²π(πΉβπ) β π’ |
16 | 12, 15 | nfan 1903 |
. . . . . . . . 9
β’
β²π(π β dom πΉ β§ (πΉβπ) β π’) |
17 | | nfv 1918 |
. . . . . . . . 9
β’
β²π(π β dom πΉ β§ (πΉβπ) β π’) |
18 | | eleq1w 2817 |
. . . . . . . . . 10
β’ (π = π β (π β dom πΉ β π β dom πΉ)) |
19 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π = π β (πΉβπ) = (πΉβπ)) |
20 | 19 | eleq1d 2819 |
. . . . . . . . . 10
β’ (π = π β ((πΉβπ) β π’ β (πΉβπ) β π’)) |
21 | 18, 20 | anbi12d 632 |
. . . . . . . . 9
β’ (π = π β ((π β dom πΉ β§ (πΉβπ) β π’) β (π β dom πΉ β§ (πΉβπ) β π’))) |
22 | 16, 17, 21 | cbvralw 3288 |
. . . . . . . 8
β’
(βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)) |
23 | 8, 22 | bitrdi 287 |
. . . . . . 7
β’ (π = π β (βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
24 | 23 | cbvrexvw 3225 |
. . . . . 6
β’
(βπ β
β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’) β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)) |
25 | 6, 24 | bitrdi 287 |
. . . . 5
β’ (π£ = π’ β (βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π£) β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
26 | 3, 25 | imbi12d 345 |
. . . 4
β’ (π£ = π’ β ((π β π£ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π£)) β (π β π’ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) |
27 | 26 | cbvralvw 3224 |
. . 3
β’
(βπ£ β
π½ (π β π£ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π£)) β βπ’ β π½ (π β π’ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
28 | 27 | 3anbi3i 1160 |
. 2
β’ ((πΉ β (π βpm β) β§ π β π β§ βπ£ β π½ (π β π£ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π£))) β (πΉ β (π βpm β) β§ π β π β§ βπ’ β π½ (π β π’ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) |
29 | 2, 28 | bitrdi 287 |
1
β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§ π β π β§ βπ’ β π½ (π β π’ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))))) |