Step | Hyp | Ref
| Expression |
1 | | preimaiocmnf.1 |
. . . 4
β’ (π β πΉ:π΄βΆβ) |
2 | 1 | ffnd 6670 |
. . 3
β’ (π β πΉ Fn π΄) |
3 | | fncnvima2 7012 |
. . 3
β’ (πΉ Fn π΄ β (β‘πΉ β (-β(,]π΅)) = {π₯ β π΄ β£ (πΉβπ₯) β (-β(,]π΅)}) |
4 | 2, 3 | syl 17 |
. 2
β’ (π β (β‘πΉ β (-β(,]π΅)) = {π₯ β π΄ β£ (πΉβπ₯) β (-β(,]π΅)}) |
5 | | mnfxr 11213 |
. . . . . . . 8
β’ -β
β β* |
6 | 5 | a1i 11 |
. . . . . . 7
β’ ((π β§ (πΉβπ₯) β (-β(,]π΅)) β -β β
β*) |
7 | | preimaiocmnf.2 |
. . . . . . . 8
β’ (π β π΅ β
β*) |
8 | 7 | adantr 482 |
. . . . . . 7
β’ ((π β§ (πΉβπ₯) β (-β(,]π΅)) β π΅ β
β*) |
9 | | simpr 486 |
. . . . . . 7
β’ ((π β§ (πΉβπ₯) β (-β(,]π΅)) β (πΉβπ₯) β (-β(,]π΅)) |
10 | 6, 8, 9 | iocleubd 43804 |
. . . . . 6
β’ ((π β§ (πΉβπ₯) β (-β(,]π΅)) β (πΉβπ₯) β€ π΅) |
11 | 10 | ex 414 |
. . . . 5
β’ (π β ((πΉβπ₯) β (-β(,]π΅) β (πΉβπ₯) β€ π΅)) |
12 | 11 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β π΄) β ((πΉβπ₯) β (-β(,]π΅) β (πΉβπ₯) β€ π΅)) |
13 | 5 | a1i 11 |
. . . . . 6
β’ (((π β§ π₯ β π΄) β§ (πΉβπ₯) β€ π΅) β -β β
β*) |
14 | 7 | adantr 482 |
. . . . . . 7
β’ ((π β§ (πΉβπ₯) β€ π΅) β π΅ β
β*) |
15 | 14 | adantlr 714 |
. . . . . 6
β’ (((π β§ π₯ β π΄) β§ (πΉβπ₯) β€ π΅) β π΅ β
β*) |
16 | 1 | ffvelcdmda 7036 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β (πΉβπ₯) β β) |
17 | 16 | rexrd 11206 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β (πΉβπ₯) β
β*) |
18 | 17 | adantr 482 |
. . . . . 6
β’ (((π β§ π₯ β π΄) β§ (πΉβπ₯) β€ π΅) β (πΉβπ₯) β
β*) |
19 | 16 | mnfltd 13046 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β -β < (πΉβπ₯)) |
20 | 19 | adantr 482 |
. . . . . 6
β’ (((π β§ π₯ β π΄) β§ (πΉβπ₯) β€ π΅) β -β < (πΉβπ₯)) |
21 | | simpr 486 |
. . . . . 6
β’ (((π β§ π₯ β π΄) β§ (πΉβπ₯) β€ π΅) β (πΉβπ₯) β€ π΅) |
22 | 13, 15, 18, 20, 21 | eliocd 43752 |
. . . . 5
β’ (((π β§ π₯ β π΄) β§ (πΉβπ₯) β€ π΅) β (πΉβπ₯) β (-β(,]π΅)) |
23 | 22 | ex 414 |
. . . 4
β’ ((π β§ π₯ β π΄) β ((πΉβπ₯) β€ π΅ β (πΉβπ₯) β (-β(,]π΅))) |
24 | 12, 23 | impbid 211 |
. . 3
β’ ((π β§ π₯ β π΄) β ((πΉβπ₯) β (-β(,]π΅) β (πΉβπ₯) β€ π΅)) |
25 | 24 | rabbidva 3415 |
. 2
β’ (π β {π₯ β π΄ β£ (πΉβπ₯) β (-β(,]π΅)} = {π₯ β π΄ β£ (πΉβπ₯) β€ π΅}) |
26 | 4, 25 | eqtrd 2777 |
1
β’ (π β (β‘πΉ β (-β(,]π΅)) = {π₯ β π΄ β£ (πΉβπ₯) β€ π΅}) |