Step | Hyp | Ref
| Expression |
1 | | o1co.2 |
. . . 4
β’ (π β πΉ β π(1)) |
2 | | o1co.1 |
. . . . 5
β’ (π β πΉ:π΄βΆβ) |
3 | 2 | fdmd 6680 |
. . . . . 6
β’ (π β dom πΉ = π΄) |
4 | | o1dm 15418 |
. . . . . . 7
β’ (πΉ β π(1) β dom
πΉ β
β) |
5 | 1, 4 | syl 17 |
. . . . . 6
β’ (π β dom πΉ β β) |
6 | 3, 5 | eqsstrrd 3984 |
. . . . 5
β’ (π β π΄ β β) |
7 | | elo12 15415 |
. . . . 5
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β (πΉ β π(1) β βπ β β βπ β β βπ§ β π΄ (π β€ π§ β (absβ(πΉβπ§)) β€ π))) |
8 | 2, 6, 7 | syl2anc 585 |
. . . 4
β’ (π β (πΉ β π(1) β βπ β β βπ β β βπ§ β π΄ (π β€ π§ β (absβ(πΉβπ§)) β€ π))) |
9 | 1, 8 | mpbid 231 |
. . 3
β’ (π β βπ β β βπ β β βπ§ β π΄ (π β€ π§ β (absβ(πΉβπ§)) β€ π)) |
10 | | o1co.5 |
. . . . 5
β’ ((π β§ π β β) β βπ₯ β β βπ¦ β π΅ (π₯ β€ π¦ β π β€ (πΊβπ¦))) |
11 | | reeanv 3216 |
. . . . . 6
β’
(βπ₯ β
β βπ β
β (βπ¦ β
π΅ (π₯ β€ π¦ β π β€ (πΊβπ¦)) β§ βπ§ β π΄ (π β€ π§ β (absβ(πΉβπ§)) β€ π)) β (βπ₯ β β βπ¦ β π΅ (π₯ β€ π¦ β π β€ (πΊβπ¦)) β§ βπ β β βπ§ β π΄ (π β€ π§ β (absβ(πΉβπ§)) β€ π))) |
12 | | o1co.3 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΊ:π΅βΆπ΄) |
13 | 12 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β β) β§ π₯ β β) β§ π β β) β πΊ:π΅βΆπ΄) |
14 | 13 | ffvelcdmda 7036 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β β) β§ π₯ β β) β§ π β β) β§ π¦ β π΅) β (πΊβπ¦) β π΄) |
15 | | breq2 5110 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = (πΊβπ¦) β (π β€ π§ β π β€ (πΊβπ¦))) |
16 | | 2fveq3 6848 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ = (πΊβπ¦) β (absβ(πΉβπ§)) = (absβ(πΉβ(πΊβπ¦)))) |
17 | 16 | breq1d 5116 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = (πΊβπ¦) β ((absβ(πΉβπ§)) β€ π β (absβ(πΉβ(πΊβπ¦))) β€ π)) |
18 | 15, 17 | imbi12d 345 |
. . . . . . . . . . . . . . . 16
β’ (π§ = (πΊβπ¦) β ((π β€ π§ β (absβ(πΉβπ§)) β€ π) β (π β€ (πΊβπ¦) β (absβ(πΉβ(πΊβπ¦))) β€ π))) |
19 | 18 | rspcva 3578 |
. . . . . . . . . . . . . . 15
β’ (((πΊβπ¦) β π΄ β§ βπ§ β π΄ (π β€ π§ β (absβ(πΉβπ§)) β€ π)) β (π β€ (πΊβπ¦) β (absβ(πΉβ(πΊβπ¦))) β€ π)) |
20 | 14, 19 | sylan 581 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π β β) β§ π₯ β β) β§ π β β) β§ π¦ β π΅) β§ βπ§ β π΄ (π β€ π§ β (absβ(πΉβπ§)) β€ π)) β (π β€ (πΊβπ¦) β (absβ(πΉβ(πΊβπ¦))) β€ π)) |
21 | 20 | an32s 651 |
. . . . . . . . . . . . 13
β’
((((((π β§ π β β) β§ π₯ β β) β§ π β β) β§
βπ§ β π΄ (π β€ π§ β (absβ(πΉβπ§)) β€ π)) β§ π¦ β π΅) β (π β€ (πΊβπ¦) β (absβ(πΉβ(πΊβπ¦))) β€ π)) |
22 | 13 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β β) β§ π₯ β β) β§ π β β) β§
βπ§ β π΄ (π β€ π§ β (absβ(πΉβπ§)) β€ π)) β πΊ:π΅βΆπ΄) |
23 | | fvco3 6941 |
. . . . . . . . . . . . . . . 16
β’ ((πΊ:π΅βΆπ΄ β§ π¦ β π΅) β ((πΉ β πΊ)βπ¦) = (πΉβ(πΊβπ¦))) |
24 | 22, 23 | sylan 581 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ π β β) β§ π₯ β β) β§ π β β) β§
βπ§ β π΄ (π β€ π§ β (absβ(πΉβπ§)) β€ π)) β§ π¦ β π΅) β ((πΉ β πΊ)βπ¦) = (πΉβ(πΊβπ¦))) |
25 | 24 | fveq2d 6847 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π β β) β§ π₯ β β) β§ π β β) β§
βπ§ β π΄ (π β€ π§ β (absβ(πΉβπ§)) β€ π)) β§ π¦ β π΅) β (absβ((πΉ β πΊ)βπ¦)) = (absβ(πΉβ(πΊβπ¦)))) |
26 | 25 | breq1d 5116 |
. . . . . . . . . . . . 13
β’
((((((π β§ π β β) β§ π₯ β β) β§ π β β) β§
βπ§ β π΄ (π β€ π§ β (absβ(πΉβπ§)) β€ π)) β§ π¦ β π΅) β ((absβ((πΉ β πΊ)βπ¦)) β€ π β (absβ(πΉβ(πΊβπ¦))) β€ π)) |
27 | 21, 26 | sylibrd 259 |
. . . . . . . . . . . 12
β’
((((((π β§ π β β) β§ π₯ β β) β§ π β β) β§
βπ§ β π΄ (π β€ π§ β (absβ(πΉβπ§)) β€ π)) β§ π¦ β π΅) β (π β€ (πΊβπ¦) β (absβ((πΉ β πΊ)βπ¦)) β€ π)) |
28 | 27 | imim2d 57 |
. . . . . . . . . . 11
β’
((((((π β§ π β β) β§ π₯ β β) β§ π β β) β§
βπ§ β π΄ (π β€ π§ β (absβ(πΉβπ§)) β€ π)) β§ π¦ β π΅) β ((π₯ β€ π¦ β π β€ (πΊβπ¦)) β (π₯ β€ π¦ β (absβ((πΉ β πΊ)βπ¦)) β€ π))) |
29 | 28 | ralimdva 3161 |
. . . . . . . . . 10
β’
(((((π β§ π β β) β§ π₯ β β) β§ π β β) β§
βπ§ β π΄ (π β€ π§ β (absβ(πΉβπ§)) β€ π)) β (βπ¦ β π΅ (π₯ β€ π¦ β π β€ (πΊβπ¦)) β βπ¦ β π΅ (π₯ β€ π¦ β (absβ((πΉ β πΊ)βπ¦)) β€ π))) |
30 | 29 | expimpd 455 |
. . . . . . . . 9
β’ ((((π β§ π β β) β§ π₯ β β) β§ π β β) β ((βπ§ β π΄ (π β€ π§ β (absβ(πΉβπ§)) β€ π) β§ βπ¦ β π΅ (π₯ β€ π¦ β π β€ (πΊβπ¦))) β βπ¦ β π΅ (π₯ β€ π¦ β (absβ((πΉ β πΊ)βπ¦)) β€ π))) |
31 | 30 | ancomsd 467 |
. . . . . . . 8
β’ ((((π β§ π β β) β§ π₯ β β) β§ π β β) β ((βπ¦ β π΅ (π₯ β€ π¦ β π β€ (πΊβπ¦)) β§ βπ§ β π΄ (π β€ π§ β (absβ(πΉβπ§)) β€ π)) β βπ¦ β π΅ (π₯ β€ π¦ β (absβ((πΉ β πΊ)βπ¦)) β€ π))) |
32 | 31 | reximdva 3162 |
. . . . . . 7
β’ (((π β§ π β β) β§ π₯ β β) β (βπ β β (βπ¦ β π΅ (π₯ β€ π¦ β π β€ (πΊβπ¦)) β§ βπ§ β π΄ (π β€ π§ β (absβ(πΉβπ§)) β€ π)) β βπ β β βπ¦ β π΅ (π₯ β€ π¦ β (absβ((πΉ β πΊ)βπ¦)) β€ π))) |
33 | 32 | reximdva 3162 |
. . . . . 6
β’ ((π β§ π β β) β (βπ₯ β β βπ β β (βπ¦ β π΅ (π₯ β€ π¦ β π β€ (πΊβπ¦)) β§ βπ§ β π΄ (π β€ π§ β (absβ(πΉβπ§)) β€ π)) β βπ₯ β β βπ β β βπ¦ β π΅ (π₯ β€ π¦ β (absβ((πΉ β πΊ)βπ¦)) β€ π))) |
34 | 11, 33 | biimtrrid 242 |
. . . . 5
β’ ((π β§ π β β) β ((βπ₯ β β βπ¦ β π΅ (π₯ β€ π¦ β π β€ (πΊβπ¦)) β§ βπ β β βπ§ β π΄ (π β€ π§ β (absβ(πΉβπ§)) β€ π)) β βπ₯ β β βπ β β βπ¦ β π΅ (π₯ β€ π¦ β (absβ((πΉ β πΊ)βπ¦)) β€ π))) |
35 | 10, 34 | mpand 694 |
. . . 4
β’ ((π β§ π β β) β (βπ β β βπ§ β π΄ (π β€ π§ β (absβ(πΉβπ§)) β€ π) β βπ₯ β β βπ β β βπ¦ β π΅ (π₯ β€ π¦ β (absβ((πΉ β πΊ)βπ¦)) β€ π))) |
36 | 35 | rexlimdva 3149 |
. . 3
β’ (π β (βπ β β βπ β β βπ§ β π΄ (π β€ π§ β (absβ(πΉβπ§)) β€ π) β βπ₯ β β βπ β β βπ¦ β π΅ (π₯ β€ π¦ β (absβ((πΉ β πΊ)βπ¦)) β€ π))) |
37 | 9, 36 | mpd 15 |
. 2
β’ (π β βπ₯ β β βπ β β βπ¦ β π΅ (π₯ β€ π¦ β (absβ((πΉ β πΊ)βπ¦)) β€ π)) |
38 | | fco 6693 |
. . . 4
β’ ((πΉ:π΄βΆβ β§ πΊ:π΅βΆπ΄) β (πΉ β πΊ):π΅βΆβ) |
39 | 2, 12, 38 | syl2anc 585 |
. . 3
β’ (π β (πΉ β πΊ):π΅βΆβ) |
40 | | o1co.4 |
. . 3
β’ (π β π΅ β β) |
41 | | elo12 15415 |
. . 3
β’ (((πΉ β πΊ):π΅βΆβ β§ π΅ β β) β ((πΉ β πΊ) β π(1) β βπ₯ β β βπ β β βπ¦ β π΅ (π₯ β€ π¦ β (absβ((πΉ β πΊ)βπ¦)) β€ π))) |
42 | 39, 40, 41 | syl2anc 585 |
. 2
β’ (π β ((πΉ β πΊ) β π(1) β βπ₯ β β βπ β β βπ¦ β π΅ (π₯ β€ π¦ β (absβ((πΉ β πΊ)βπ¦)) β€ π))) |
43 | 37, 42 | mpbird 257 |
1
β’ (π β (πΉ β πΊ) β π(1)) |