Step | Hyp | Ref
| Expression |
1 | | preimaicomnf.1 |
. . . 4
β’ (π β πΉ:π΄βΆβ*) |
2 | 1 | ffnd 6670 |
. . 3
β’ (π β πΉ Fn π΄) |
3 | | fncnvima2 7012 |
. . 3
β’ (πΉ Fn π΄ β (β‘πΉ β (-β[,)π΅)) = {π₯ β π΄ β£ (πΉβπ₯) β (-β[,)π΅)}) |
4 | 2, 3 | syl 17 |
. 2
β’ (π β (β‘πΉ β (-β[,)π΅)) = {π₯ β π΄ β£ (πΉβπ₯) β (-β[,)π΅)}) |
5 | | mnfxr 11217 |
. . . . . . 7
β’ -β
β β* |
6 | 5 | a1i 11 |
. . . . . 6
β’ (((π β§ π₯ β π΄) β§ (πΉβπ₯) β (-β[,)π΅)) β -β β
β*) |
7 | | preimaicomnf.2 |
. . . . . . 7
β’ (π β π΅ β
β*) |
8 | 7 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π₯ β π΄) β§ (πΉβπ₯) β (-β[,)π΅)) β π΅ β
β*) |
9 | | simpr 486 |
. . . . . 6
β’ (((π β§ π₯ β π΄) β§ (πΉβπ₯) β (-β[,)π΅)) β (πΉβπ₯) β (-β[,)π΅)) |
10 | | icoltub 43832 |
. . . . . 6
β’
((-β β β* β§ π΅ β β* β§ (πΉβπ₯) β (-β[,)π΅)) β (πΉβπ₯) < π΅) |
11 | 6, 8, 9, 10 | syl3anc 1372 |
. . . . 5
β’ (((π β§ π₯ β π΄) β§ (πΉβπ₯) β (-β[,)π΅)) β (πΉβπ₯) < π΅) |
12 | 11 | ex 414 |
. . . 4
β’ ((π β§ π₯ β π΄) β ((πΉβπ₯) β (-β[,)π΅) β (πΉβπ₯) < π΅)) |
13 | 5 | a1i 11 |
. . . . . 6
β’ (((π β§ π₯ β π΄) β§ (πΉβπ₯) < π΅) β -β β
β*) |
14 | 7 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π₯ β π΄) β§ (πΉβπ₯) < π΅) β π΅ β
β*) |
15 | 1 | ffvelcdmda 7036 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β (πΉβπ₯) β
β*) |
16 | 15 | adantr 482 |
. . . . . 6
β’ (((π β§ π₯ β π΄) β§ (πΉβπ₯) < π΅) β (πΉβπ₯) β
β*) |
17 | 15 | mnfled 13061 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β -β β€ (πΉβπ₯)) |
18 | 17 | adantr 482 |
. . . . . 6
β’ (((π β§ π₯ β π΄) β§ (πΉβπ₯) < π΅) β -β β€ (πΉβπ₯)) |
19 | | simpr 486 |
. . . . . 6
β’ (((π β§ π₯ β π΄) β§ (πΉβπ₯) < π΅) β (πΉβπ₯) < π΅) |
20 | 13, 14, 16, 18, 19 | elicod 13320 |
. . . . 5
β’ (((π β§ π₯ β π΄) β§ (πΉβπ₯) < π΅) β (πΉβπ₯) β (-β[,)π΅)) |
21 | 20 | ex 414 |
. . . 4
β’ ((π β§ π₯ β π΄) β ((πΉβπ₯) < π΅ β (πΉβπ₯) β (-β[,)π΅))) |
22 | 12, 21 | impbid 211 |
. . 3
β’ ((π β§ π₯ β π΄) β ((πΉβπ₯) β (-β[,)π΅) β (πΉβπ₯) < π΅)) |
23 | 22 | rabbidva 3413 |
. 2
β’ (π β {π₯ β π΄ β£ (πΉβπ₯) β (-β[,)π΅)} = {π₯ β π΄ β£ (πΉβπ₯) < π΅}) |
24 | 4, 23 | eqtrd 2773 |
1
β’ (π β (β‘πΉ β (-β[,)π΅)) = {π₯ β π΄ β£ (πΉβπ₯) < π΅}) |