Step | Hyp | Ref
| Expression |
1 | | lo1f 15409 |
. . . 4
β’ (πΉ β β€π(1) β
πΉ:dom πΉβΆβ) |
2 | | lo1bdd 15411 |
. . . 4
β’ ((πΉ β β€π(1) β§
πΉ:dom πΉβΆβ) β βπ₯ β β βπ β β βπ¦ β dom πΉ(π₯ β€ π¦ β (πΉβπ¦) β€ π)) |
3 | 1, 2 | mpdan 686 |
. . 3
β’ (πΉ β β€π(1) β
βπ₯ β β
βπ β β
βπ¦ β dom πΉ(π₯ β€ π¦ β (πΉβπ¦) β€ π)) |
4 | | inss1 4192 |
. . . . . . 7
β’ (dom
πΉ β© π΄) β dom πΉ |
5 | | ssralv 4014 |
. . . . . . 7
β’ ((dom
πΉ β© π΄) β dom πΉ β (βπ¦ β dom πΉ(π₯ β€ π¦ β (πΉβπ¦) β€ π) β βπ¦ β (dom πΉ β© π΄)(π₯ β€ π¦ β (πΉβπ¦) β€ π))) |
6 | 4, 5 | ax-mp 5 |
. . . . . 6
β’
(βπ¦ β
dom πΉ(π₯ β€ π¦ β (πΉβπ¦) β€ π) β βπ¦ β (dom πΉ β© π΄)(π₯ β€ π¦ β (πΉβπ¦) β€ π)) |
7 | | elinel2 4160 |
. . . . . . . . . 10
β’ (π¦ β (dom πΉ β© π΄) β π¦ β π΄) |
8 | 7 | fvresd 6866 |
. . . . . . . . 9
β’ (π¦ β (dom πΉ β© π΄) β ((πΉ βΎ π΄)βπ¦) = (πΉβπ¦)) |
9 | 8 | breq1d 5119 |
. . . . . . . 8
β’ (π¦ β (dom πΉ β© π΄) β (((πΉ βΎ π΄)βπ¦) β€ π β (πΉβπ¦) β€ π)) |
10 | 9 | imbi2d 341 |
. . . . . . 7
β’ (π¦ β (dom πΉ β© π΄) β ((π₯ β€ π¦ β ((πΉ βΎ π΄)βπ¦) β€ π) β (π₯ β€ π¦ β (πΉβπ¦) β€ π))) |
11 | 10 | ralbiia 3091 |
. . . . . 6
β’
(βπ¦ β
(dom πΉ β© π΄)(π₯ β€ π¦ β ((πΉ βΎ π΄)βπ¦) β€ π) β βπ¦ β (dom πΉ β© π΄)(π₯ β€ π¦ β (πΉβπ¦) β€ π)) |
12 | 6, 11 | sylibr 233 |
. . . . 5
β’
(βπ¦ β
dom πΉ(π₯ β€ π¦ β (πΉβπ¦) β€ π) β βπ¦ β (dom πΉ β© π΄)(π₯ β€ π¦ β ((πΉ βΎ π΄)βπ¦) β€ π)) |
13 | 12 | reximi 3084 |
. . . 4
β’
(βπ β
β βπ¦ β
dom πΉ(π₯ β€ π¦ β (πΉβπ¦) β€ π) β βπ β β βπ¦ β (dom πΉ β© π΄)(π₯ β€ π¦ β ((πΉ βΎ π΄)βπ¦) β€ π)) |
14 | 13 | reximi 3084 |
. . 3
β’
(βπ₯ β
β βπ β
β βπ¦ β
dom πΉ(π₯ β€ π¦ β (πΉβπ¦) β€ π) β βπ₯ β β βπ β β βπ¦ β (dom πΉ β© π΄)(π₯ β€ π¦ β ((πΉ βΎ π΄)βπ¦) β€ π)) |
15 | 3, 14 | syl 17 |
. 2
β’ (πΉ β β€π(1) β
βπ₯ β β
βπ β β
βπ¦ β (dom πΉ β© π΄)(π₯ β€ π¦ β ((πΉ βΎ π΄)βπ¦) β€ π)) |
16 | | fssres 6712 |
. . . . 5
β’ ((πΉ:dom πΉβΆβ β§ (dom πΉ β© π΄) β dom πΉ) β (πΉ βΎ (dom πΉ β© π΄)):(dom πΉ β© π΄)βΆβ) |
17 | 1, 4, 16 | sylancl 587 |
. . . 4
β’ (πΉ β β€π(1) β
(πΉ βΎ (dom πΉ β© π΄)):(dom πΉ β© π΄)βΆβ) |
18 | | resres 5954 |
. . . . . 6
β’ ((πΉ βΎ dom πΉ) βΎ π΄) = (πΉ βΎ (dom πΉ β© π΄)) |
19 | | ffn 6672 |
. . . . . . . 8
β’ (πΉ:dom πΉβΆβ β πΉ Fn dom πΉ) |
20 | | fnresdm 6624 |
. . . . . . . 8
β’ (πΉ Fn dom πΉ β (πΉ βΎ dom πΉ) = πΉ) |
21 | 1, 19, 20 | 3syl 18 |
. . . . . . 7
β’ (πΉ β β€π(1) β
(πΉ βΎ dom πΉ) = πΉ) |
22 | 21 | reseq1d 5940 |
. . . . . 6
β’ (πΉ β β€π(1) β
((πΉ βΎ dom πΉ) βΎ π΄) = (πΉ βΎ π΄)) |
23 | 18, 22 | eqtr3id 2787 |
. . . . 5
β’ (πΉ β β€π(1) β
(πΉ βΎ (dom πΉ β© π΄)) = (πΉ βΎ π΄)) |
24 | 23 | feq1d 6657 |
. . . 4
β’ (πΉ β β€π(1) β
((πΉ βΎ (dom πΉ β© π΄)):(dom πΉ β© π΄)βΆβ β (πΉ βΎ π΄):(dom πΉ β© π΄)βΆβ)) |
25 | 17, 24 | mpbid 231 |
. . 3
β’ (πΉ β β€π(1) β
(πΉ βΎ π΄):(dom πΉ β© π΄)βΆβ) |
26 | | lo1dm 15410 |
. . . 4
β’ (πΉ β β€π(1) β
dom πΉ β
β) |
27 | 4, 26 | sstrid 3959 |
. . 3
β’ (πΉ β β€π(1) β
(dom πΉ β© π΄) β
β) |
28 | | ello12 15407 |
. . 3
β’ (((πΉ βΎ π΄):(dom πΉ β© π΄)βΆβ β§ (dom πΉ β© π΄) β β) β ((πΉ βΎ π΄) β β€π(1) β
βπ₯ β β
βπ β β
βπ¦ β (dom πΉ β© π΄)(π₯ β€ π¦ β ((πΉ βΎ π΄)βπ¦) β€ π))) |
29 | 25, 27, 28 | syl2anc 585 |
. 2
β’ (πΉ β β€π(1) β
((πΉ βΎ π΄) β β€π(1) β
βπ₯ β β
βπ β β
βπ¦ β (dom πΉ β© π΄)(π₯ β€ π¦ β ((πΉ βΎ π΄)βπ¦) β€ π))) |
30 | 15, 29 | mpbird 257 |
1
β’ (πΉ β β€π(1) β
(πΉ βΎ π΄) β
β€π(1)) |