Step | Hyp | Ref
| Expression |
1 | | elbigo 47190 |
. . . 4
β’ (πΉ β (ΞβπΊ) β (πΉ β (β βpm
β) β§ πΊ β
(β βpm β) β§ βπ₯ β β βπ β β βπ¦ β (dom πΉ β© (π₯[,)+β))(πΉβπ¦) β€ (π Β· (πΊβπ¦)))) |
2 | | df-3an 1089 |
. . . 4
β’ ((πΉ β (β
βpm β) β§ πΊ β (β βpm
β) β§ βπ₯
β β βπ
β β βπ¦
β (dom πΉ β© (π₯[,)+β))(πΉβπ¦) β€ (π Β· (πΊβπ¦))) β ((πΉ β (β βpm
β) β§ πΊ β
(β βpm β)) β§ βπ₯ β β βπ β β βπ¦ β (dom πΉ β© (π₯[,)+β))(πΉβπ¦) β€ (π Β· (πΊβπ¦)))) |
3 | 1, 2 | bitri 274 |
. . 3
β’ (πΉ β (ΞβπΊ) β ((πΉ β (β βpm
β) β§ πΊ β
(β βpm β)) β§ βπ₯ β β βπ β β βπ¦ β (dom πΉ β© (π₯[,)+β))(πΉβπ¦) β€ (π Β· (πΊβπ¦)))) |
4 | | reex 11197 |
. . . . . . 7
β’ β
β V |
5 | 4, 4 | pm3.2i 471 |
. . . . . 6
β’ (β
β V β§ β β V) |
6 | 5 | a1i 11 |
. . . . 5
β’ (((πΊ:π΄βΆβ β§ π΄ β β) β§ (πΉ:π΅βΆβ β§ π΅ β π΄)) β (β β V β§ β
β V)) |
7 | | simpl 483 |
. . . . . 6
β’ ((πΉ:π΅βΆβ β§ π΅ β π΄) β πΉ:π΅βΆβ) |
8 | 7 | adantl 482 |
. . . . 5
β’ (((πΊ:π΄βΆβ β§ π΄ β β) β§ (πΉ:π΅βΆβ β§ π΅ β π΄)) β πΉ:π΅βΆβ) |
9 | | sstr2 3988 |
. . . . . . . 8
β’ (π΅ β π΄ β (π΄ β β β π΅ β β)) |
10 | 9 | adantld 491 |
. . . . . . 7
β’ (π΅ β π΄ β ((πΊ:π΄βΆβ β§ π΄ β β) β π΅ β β)) |
11 | 10 | adantl 482 |
. . . . . 6
β’ ((πΉ:π΅βΆβ β§ π΅ β π΄) β ((πΊ:π΄βΆβ β§ π΄ β β) β π΅ β β)) |
12 | 11 | impcom 408 |
. . . . 5
β’ (((πΊ:π΄βΆβ β§ π΄ β β) β§ (πΉ:π΅βΆβ β§ π΅ β π΄)) β π΅ β β) |
13 | | elpm2r 8835 |
. . . . 5
β’
(((β β V β§ β β V) β§ (πΉ:π΅βΆβ β§ π΅ β β)) β πΉ β (β βpm
β)) |
14 | 6, 8, 12, 13 | syl12anc 835 |
. . . 4
β’ (((πΊ:π΄βΆβ β§ π΄ β β) β§ (πΉ:π΅βΆβ β§ π΅ β π΄)) β πΉ β (β βpm
β)) |
15 | | simpl 483 |
. . . . 5
β’ (((πΊ:π΄βΆβ β§ π΄ β β) β§ (πΉ:π΅βΆβ β§ π΅ β π΄)) β (πΊ:π΄βΆβ β§ π΄ β β)) |
16 | | elpm2r 8835 |
. . . . 5
β’
(((β β V β§ β β V) β§ (πΊ:π΄βΆβ β§ π΄ β β)) β πΊ β (β βpm
β)) |
17 | 6, 15, 16 | syl2anc 584 |
. . . 4
β’ (((πΊ:π΄βΆβ β§ π΄ β β) β§ (πΉ:π΅βΆβ β§ π΅ β π΄)) β πΊ β (β βpm
β)) |
18 | | ibar 529 |
. . . . 5
β’ ((πΉ β (β
βpm β) β§ πΊ β (β βpm
β)) β (βπ₯
β β βπ
β β βπ¦
β (dom πΉ β© (π₯[,)+β))(πΉβπ¦) β€ (π Β· (πΊβπ¦)) β ((πΉ β (β βpm
β) β§ πΊ β
(β βpm β)) β§ βπ₯ β β βπ β β βπ¦ β (dom πΉ β© (π₯[,)+β))(πΉβπ¦) β€ (π Β· (πΊβπ¦))))) |
19 | 18 | bicomd 222 |
. . . 4
β’ ((πΉ β (β
βpm β) β§ πΊ β (β βpm
β)) β (((πΉ
β (β βpm β) β§ πΊ β (β βpm
β)) β§ βπ₯
β β βπ
β β βπ¦
β (dom πΉ β© (π₯[,)+β))(πΉβπ¦) β€ (π Β· (πΊβπ¦))) β βπ₯ β β βπ β β βπ¦ β (dom πΉ β© (π₯[,)+β))(πΉβπ¦) β€ (π Β· (πΊβπ¦)))) |
20 | 14, 17, 19 | syl2anc 584 |
. . 3
β’ (((πΊ:π΄βΆβ β§ π΄ β β) β§ (πΉ:π΅βΆβ β§ π΅ β π΄)) β (((πΉ β (β βpm
β) β§ πΊ β
(β βpm β)) β§ βπ₯ β β βπ β β βπ¦ β (dom πΉ β© (π₯[,)+β))(πΉβπ¦) β€ (π Β· (πΊβπ¦))) β βπ₯ β β βπ β β βπ¦ β (dom πΉ β© (π₯[,)+β))(πΉβπ¦) β€ (π Β· (πΊβπ¦)))) |
21 | 3, 20 | bitrid 282 |
. 2
β’ (((πΊ:π΄βΆβ β§ π΄ β β) β§ (πΉ:π΅βΆβ β§ π΅ β π΄)) β (πΉ β (ΞβπΊ) β βπ₯ β β βπ β β βπ¦ β (dom πΉ β© (π₯[,)+β))(πΉβπ¦) β€ (π Β· (πΊβπ¦)))) |
22 | | elin 3963 |
. . . . . . . 8
β’ (π¦ β (dom πΉ β© (π₯[,)+β)) β (π¦ β dom πΉ β§ π¦ β (π₯[,)+β))) |
23 | | fdm 6723 |
. . . . . . . . . . . . 13
β’ (πΉ:π΅βΆβ β dom πΉ = π΅) |
24 | 23 | ad2antrl 726 |
. . . . . . . . . . . 12
β’ (((πΊ:π΄βΆβ β§ π΄ β β) β§ (πΉ:π΅βΆβ β§ π΅ β π΄)) β dom πΉ = π΅) |
25 | 24 | ad2antrr 724 |
. . . . . . . . . . 11
β’
(((((πΊ:π΄βΆβ β§ π΄ β β) β§ (πΉ:π΅βΆβ β§ π΅ β π΄)) β§ π₯ β β) β§ π β β) β dom πΉ = π΅) |
26 | 25 | eleq2d 2819 |
. . . . . . . . . 10
β’
(((((πΊ:π΄βΆβ β§ π΄ β β) β§ (πΉ:π΅βΆβ β§ π΅ β π΄)) β§ π₯ β β) β§ π β β) β (π¦ β dom πΉ β π¦ β π΅)) |
27 | 26 | anbi1d 630 |
. . . . . . . . 9
β’
(((((πΊ:π΄βΆβ β§ π΄ β β) β§ (πΉ:π΅βΆβ β§ π΅ β π΄)) β§ π₯ β β) β§ π β β) β ((π¦ β dom πΉ β§ π¦ β (π₯[,)+β)) β (π¦ β π΅ β§ π¦ β (π₯[,)+β)))) |
28 | | elicopnf 13418 |
. . . . . . . . . . . 12
β’ (π₯ β β β (π¦ β (π₯[,)+β) β (π¦ β β β§ π₯ β€ π¦))) |
29 | 28 | ad3antlr 729 |
. . . . . . . . . . 11
β’
((((((πΊ:π΄βΆβ β§ π΄ β β) β§ (πΉ:π΅βΆβ β§ π΅ β π΄)) β§ π₯ β β) β§ π β β) β§ π¦ β π΅) β (π¦ β (π₯[,)+β) β (π¦ β β β§ π₯ β€ π¦))) |
30 | 12 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’
(((((πΊ:π΄βΆβ β§ π΄ β β) β§ (πΉ:π΅βΆβ β§ π΅ β π΄)) β§ π₯ β β) β§ π β β) β π΅ β β) |
31 | 30 | sselda 3981 |
. . . . . . . . . . . 12
β’
((((((πΊ:π΄βΆβ β§ π΄ β β) β§ (πΉ:π΅βΆβ β§ π΅ β π΄)) β§ π₯ β β) β§ π β β) β§ π¦ β π΅) β π¦ β β) |
32 | 31 | biantrurd 533 |
. . . . . . . . . . 11
β’
((((((πΊ:π΄βΆβ β§ π΄ β β) β§ (πΉ:π΅βΆβ β§ π΅ β π΄)) β§ π₯ β β) β§ π β β) β§ π¦ β π΅) β (π₯ β€ π¦ β (π¦ β β β§ π₯ β€ π¦))) |
33 | 29, 32 | bitr4d 281 |
. . . . . . . . . 10
β’
((((((πΊ:π΄βΆβ β§ π΄ β β) β§ (πΉ:π΅βΆβ β§ π΅ β π΄)) β§ π₯ β β) β§ π β β) β§ π¦ β π΅) β (π¦ β (π₯[,)+β) β π₯ β€ π¦)) |
34 | 33 | pm5.32da 579 |
. . . . . . . . 9
β’
(((((πΊ:π΄βΆβ β§ π΄ β β) β§ (πΉ:π΅βΆβ β§ π΅ β π΄)) β§ π₯ β β) β§ π β β) β ((π¦ β π΅ β§ π¦ β (π₯[,)+β)) β (π¦ β π΅ β§ π₯ β€ π¦))) |
35 | 27, 34 | bitrd 278 |
. . . . . . . 8
β’
(((((πΊ:π΄βΆβ β§ π΄ β β) β§ (πΉ:π΅βΆβ β§ π΅ β π΄)) β§ π₯ β β) β§ π β β) β ((π¦ β dom πΉ β§ π¦ β (π₯[,)+β)) β (π¦ β π΅ β§ π₯ β€ π¦))) |
36 | 22, 35 | bitrid 282 |
. . . . . . 7
β’
(((((πΊ:π΄βΆβ β§ π΄ β β) β§ (πΉ:π΅βΆβ β§ π΅ β π΄)) β§ π₯ β β) β§ π β β) β (π¦ β (dom πΉ β© (π₯[,)+β)) β (π¦ β π΅ β§ π₯ β€ π¦))) |
37 | 36 | imbi1d 341 |
. . . . . 6
β’
(((((πΊ:π΄βΆβ β§ π΄ β β) β§ (πΉ:π΅βΆβ β§ π΅ β π΄)) β§ π₯ β β) β§ π β β) β ((π¦ β (dom πΉ β© (π₯[,)+β)) β (πΉβπ¦) β€ (π Β· (πΊβπ¦))) β ((π¦ β π΅ β§ π₯ β€ π¦) β (πΉβπ¦) β€ (π Β· (πΊβπ¦))))) |
38 | | impexp 451 |
. . . . . 6
β’ (((π¦ β π΅ β§ π₯ β€ π¦) β (πΉβπ¦) β€ (π Β· (πΊβπ¦))) β (π¦ β π΅ β (π₯ β€ π¦ β (πΉβπ¦) β€ (π Β· (πΊβπ¦))))) |
39 | 37, 38 | bitrdi 286 |
. . . . 5
β’
(((((πΊ:π΄βΆβ β§ π΄ β β) β§ (πΉ:π΅βΆβ β§ π΅ β π΄)) β§ π₯ β β) β§ π β β) β ((π¦ β (dom πΉ β© (π₯[,)+β)) β (πΉβπ¦) β€ (π Β· (πΊβπ¦))) β (π¦ β π΅ β (π₯ β€ π¦ β (πΉβπ¦) β€ (π Β· (πΊβπ¦)))))) |
40 | 39 | ralbidv2 3173 |
. . . 4
β’
(((((πΊ:π΄βΆβ β§ π΄ β β) β§ (πΉ:π΅βΆβ β§ π΅ β π΄)) β§ π₯ β β) β§ π β β) β (βπ¦ β (dom πΉ β© (π₯[,)+β))(πΉβπ¦) β€ (π Β· (πΊβπ¦)) β βπ¦ β π΅ (π₯ β€ π¦ β (πΉβπ¦) β€ (π Β· (πΊβπ¦))))) |
41 | 40 | rexbidva 3176 |
. . 3
β’ ((((πΊ:π΄βΆβ β§ π΄ β β) β§ (πΉ:π΅βΆβ β§ π΅ β π΄)) β§ π₯ β β) β (βπ β β βπ¦ β (dom πΉ β© (π₯[,)+β))(πΉβπ¦) β€ (π Β· (πΊβπ¦)) β βπ β β βπ¦ β π΅ (π₯ β€ π¦ β (πΉβπ¦) β€ (π Β· (πΊβπ¦))))) |
42 | 41 | rexbidva 3176 |
. 2
β’ (((πΊ:π΄βΆβ β§ π΄ β β) β§ (πΉ:π΅βΆβ β§ π΅ β π΄)) β (βπ₯ β β βπ β β βπ¦ β (dom πΉ β© (π₯[,)+β))(πΉβπ¦) β€ (π Β· (πΊβπ¦)) β βπ₯ β β βπ β β βπ¦ β π΅ (π₯ β€ π¦ β (πΉβπ¦) β€ (π Β· (πΊβπ¦))))) |
43 | 21, 42 | bitrd 278 |
1
β’ (((πΊ:π΄βΆβ β§ π΄ β β) β§ (πΉ:π΅βΆβ β§ π΅ β π΄)) β (πΉ β (ΞβπΊ) β βπ₯ β β βπ β β βπ¦ β π΅ (π₯ β€ π¦ β (πΉβπ¦) β€ (π Β· (πΊβπ¦))))) |