Step | Hyp | Ref
| Expression |
1 | | lo1res 15450 |
. 2
β’ (πΉ β β€π(1) β
(πΉ βΎ (π΅[,)+β)) β
β€π(1)) |
2 | | lo1resb.1 |
. . . . . . 7
β’ (π β πΉ:π΄βΆβ) |
3 | 2 | feqmptd 6914 |
. . . . . 6
β’ (π β πΉ = (π₯ β π΄ β¦ (πΉβπ₯))) |
4 | 3 | reseq1d 5940 |
. . . . 5
β’ (π β (πΉ βΎ (π΅[,)+β)) = ((π₯ β π΄ β¦ (πΉβπ₯)) βΎ (π΅[,)+β))) |
5 | | resmpt3 5996 |
. . . . 5
β’ ((π₯ β π΄ β¦ (πΉβπ₯)) βΎ (π΅[,)+β)) = (π₯ β (π΄ β© (π΅[,)+β)) β¦ (πΉβπ₯)) |
6 | 4, 5 | eqtrdi 2789 |
. . . 4
β’ (π β (πΉ βΎ (π΅[,)+β)) = (π₯ β (π΄ β© (π΅[,)+β)) β¦ (πΉβπ₯))) |
7 | 6 | eleq1d 2819 |
. . 3
β’ (π β ((πΉ βΎ (π΅[,)+β)) β β€π(1) β
(π₯ β (π΄ β© (π΅[,)+β)) β¦ (πΉβπ₯)) β β€π(1))) |
8 | | inss1 4192 |
. . . . . 6
β’ (π΄ β© (π΅[,)+β)) β π΄ |
9 | | lo1resb.2 |
. . . . . 6
β’ (π β π΄ β β) |
10 | 8, 9 | sstrid 3959 |
. . . . 5
β’ (π β (π΄ β© (π΅[,)+β)) β
β) |
11 | | elinel1 4159 |
. . . . . 6
β’ (π₯ β (π΄ β© (π΅[,)+β)) β π₯ β π΄) |
12 | | ffvelcdm 7036 |
. . . . . 6
β’ ((πΉ:π΄βΆβ β§ π₯ β π΄) β (πΉβπ₯) β β) |
13 | 2, 11, 12 | syl2an 597 |
. . . . 5
β’ ((π β§ π₯ β (π΄ β© (π΅[,)+β))) β (πΉβπ₯) β β) |
14 | 10, 13 | ello1mpt 15412 |
. . . 4
β’ (π β ((π₯ β (π΄ β© (π΅[,)+β)) β¦ (πΉβπ₯)) β β€π(1) β
βπ¦ β β
βπ§ β β
βπ₯ β (π΄ β© (π΅[,)+β))(π¦ β€ π₯ β (πΉβπ₯) β€ π§))) |
15 | | elin 3930 |
. . . . . . . . . 10
β’ (π₯ β (π΄ β© (π΅[,)+β)) β (π₯ β π΄ β§ π₯ β (π΅[,)+β))) |
16 | 15 | imbi1i 350 |
. . . . . . . . 9
β’ ((π₯ β (π΄ β© (π΅[,)+β)) β (π¦ β€ π₯ β (πΉβπ₯) β€ π§)) β ((π₯ β π΄ β§ π₯ β (π΅[,)+β)) β (π¦ β€ π₯ β (πΉβπ₯) β€ π§))) |
17 | | impexp 452 |
. . . . . . . . 9
β’ (((π₯ β π΄ β§ π₯ β (π΅[,)+β)) β (π¦ β€ π₯ β (πΉβπ₯) β€ π§)) β (π₯ β π΄ β (π₯ β (π΅[,)+β) β (π¦ β€ π₯ β (πΉβπ₯) β€ π§)))) |
18 | 16, 17 | bitri 275 |
. . . . . . . 8
β’ ((π₯ β (π΄ β© (π΅[,)+β)) β (π¦ β€ π₯ β (πΉβπ₯) β€ π§)) β (π₯ β π΄ β (π₯ β (π΅[,)+β) β (π¦ β€ π₯ β (πΉβπ₯) β€ π§)))) |
19 | | impexp 452 |
. . . . . . . . . 10
β’ (((π₯ β (π΅[,)+β) β§ π¦ β€ π₯) β (πΉβπ₯) β€ π§) β (π₯ β (π΅[,)+β) β (π¦ β€ π₯ β (πΉβπ₯) β€ π§))) |
20 | | lo1resb.3 |
. . . . . . . . . . . . . . 15
β’ (π β π΅ β β) |
21 | 20 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π¦ β β β§ π§ β β)) β§ π₯ β π΄) β π΅ β β) |
22 | 9 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π¦ β β β§ π§ β β)) β π΄ β β) |
23 | 22 | sselda 3948 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π¦ β β β§ π§ β β)) β§ π₯ β π΄) β π₯ β β) |
24 | | elicopnf 13371 |
. . . . . . . . . . . . . . 15
β’ (π΅ β β β (π₯ β (π΅[,)+β) β (π₯ β β β§ π΅ β€ π₯))) |
25 | 24 | baibd 541 |
. . . . . . . . . . . . . 14
β’ ((π΅ β β β§ π₯ β β) β (π₯ β (π΅[,)+β) β π΅ β€ π₯)) |
26 | 21, 23, 25 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ (π¦ β β β§ π§ β β)) β§ π₯ β π΄) β (π₯ β (π΅[,)+β) β π΅ β€ π₯)) |
27 | 26 | anbi1d 631 |
. . . . . . . . . . . 12
β’ (((π β§ (π¦ β β β§ π§ β β)) β§ π₯ β π΄) β ((π₯ β (π΅[,)+β) β§ π¦ β€ π₯) β (π΅ β€ π₯ β§ π¦ β€ π₯))) |
28 | | simplrl 776 |
. . . . . . . . . . . . 13
β’ (((π β§ (π¦ β β β§ π§ β β)) β§ π₯ β π΄) β π¦ β β) |
29 | | maxle 13119 |
. . . . . . . . . . . . 13
β’ ((π΅ β β β§ π¦ β β β§ π₯ β β) β
(if(π΅ β€ π¦, π¦, π΅) β€ π₯ β (π΅ β€ π₯ β§ π¦ β€ π₯))) |
30 | 21, 28, 23, 29 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π β§ (π¦ β β β§ π§ β β)) β§ π₯ β π΄) β (if(π΅ β€ π¦, π¦, π΅) β€ π₯ β (π΅ β€ π₯ β§ π¦ β€ π₯))) |
31 | 27, 30 | bitr4d 282 |
. . . . . . . . . . 11
β’ (((π β§ (π¦ β β β§ π§ β β)) β§ π₯ β π΄) β ((π₯ β (π΅[,)+β) β§ π¦ β€ π₯) β if(π΅ β€ π¦, π¦, π΅) β€ π₯)) |
32 | 31 | imbi1d 342 |
. . . . . . . . . 10
β’ (((π β§ (π¦ β β β§ π§ β β)) β§ π₯ β π΄) β (((π₯ β (π΅[,)+β) β§ π¦ β€ π₯) β (πΉβπ₯) β€ π§) β (if(π΅ β€ π¦, π¦, π΅) β€ π₯ β (πΉβπ₯) β€ π§))) |
33 | 19, 32 | bitr3id 285 |
. . . . . . . . 9
β’ (((π β§ (π¦ β β β§ π§ β β)) β§ π₯ β π΄) β ((π₯ β (π΅[,)+β) β (π¦ β€ π₯ β (πΉβπ₯) β€ π§)) β (if(π΅ β€ π¦, π¦, π΅) β€ π₯ β (πΉβπ₯) β€ π§))) |
34 | 33 | pm5.74da 803 |
. . . . . . . 8
β’ ((π β§ (π¦ β β β§ π§ β β)) β ((π₯ β π΄ β (π₯ β (π΅[,)+β) β (π¦ β€ π₯ β (πΉβπ₯) β€ π§))) β (π₯ β π΄ β (if(π΅ β€ π¦, π¦, π΅) β€ π₯ β (πΉβπ₯) β€ π§)))) |
35 | 18, 34 | bitrid 283 |
. . . . . . 7
β’ ((π β§ (π¦ β β β§ π§ β β)) β ((π₯ β (π΄ β© (π΅[,)+β)) β (π¦ β€ π₯ β (πΉβπ₯) β€ π§)) β (π₯ β π΄ β (if(π΅ β€ π¦, π¦, π΅) β€ π₯ β (πΉβπ₯) β€ π§)))) |
36 | 35 | ralbidv2 3167 |
. . . . . 6
β’ ((π β§ (π¦ β β β§ π§ β β)) β (βπ₯ β (π΄ β© (π΅[,)+β))(π¦ β€ π₯ β (πΉβπ₯) β€ π§) β βπ₯ β π΄ (if(π΅ β€ π¦, π¦, π΅) β€ π₯ β (πΉβπ₯) β€ π§))) |
37 | 2 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π¦ β β β§ π§ β β)) β πΉ:π΄βΆβ) |
38 | | simprl 770 |
. . . . . . . 8
β’ ((π β§ (π¦ β β β§ π§ β β)) β π¦ β β) |
39 | 20 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π¦ β β β§ π§ β β)) β π΅ β β) |
40 | 38, 39 | ifcld 4536 |
. . . . . . 7
β’ ((π β§ (π¦ β β β§ π§ β β)) β if(π΅ β€ π¦, π¦, π΅) β β) |
41 | | simprr 772 |
. . . . . . 7
β’ ((π β§ (π¦ β β β§ π§ β β)) β π§ β β) |
42 | | ello12r 15408 |
. . . . . . . 8
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ (if(π΅ β€ π¦, π¦, π΅) β β β§ π§ β β) β§ βπ₯ β π΄ (if(π΅ β€ π¦, π¦, π΅) β€ π₯ β (πΉβπ₯) β€ π§)) β πΉ β β€π(1)) |
43 | 42 | 3expia 1122 |
. . . . . . 7
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ (if(π΅ β€ π¦, π¦, π΅) β β β§ π§ β β)) β (βπ₯ β π΄ (if(π΅ β€ π¦, π¦, π΅) β€ π₯ β (πΉβπ₯) β€ π§) β πΉ β β€π(1))) |
44 | 37, 22, 40, 41, 43 | syl22anc 838 |
. . . . . 6
β’ ((π β§ (π¦ β β β§ π§ β β)) β (βπ₯ β π΄ (if(π΅ β€ π¦, π¦, π΅) β€ π₯ β (πΉβπ₯) β€ π§) β πΉ β β€π(1))) |
45 | 36, 44 | sylbid 239 |
. . . . 5
β’ ((π β§ (π¦ β β β§ π§ β β)) β (βπ₯ β (π΄ β© (π΅[,)+β))(π¦ β€ π₯ β (πΉβπ₯) β€ π§) β πΉ β β€π(1))) |
46 | 45 | rexlimdvva 3202 |
. . . 4
β’ (π β (βπ¦ β β βπ§ β β βπ₯ β (π΄ β© (π΅[,)+β))(π¦ β€ π₯ β (πΉβπ₯) β€ π§) β πΉ β β€π(1))) |
47 | 14, 46 | sylbid 239 |
. . 3
β’ (π β ((π₯ β (π΄ β© (π΅[,)+β)) β¦ (πΉβπ₯)) β β€π(1) β πΉ β
β€π(1))) |
48 | 7, 47 | sylbid 239 |
. 2
β’ (π β ((πΉ βΎ (π΅[,)+β)) β β€π(1) β
πΉ β
β€π(1))) |
49 | 1, 48 | impbid2 225 |
1
β’ (π β (πΉ β β€π(1) β (πΉ βΎ (π΅[,)+β)) β
β€π(1))) |