Step | Hyp | Ref
| Expression |
1 | | feq1 6699 |
. . . . 5
β’ (π = πΊ β (π:(π‘ Γ π‘)βΆπ‘ β πΊ:(π‘ Γ π‘)βΆπ‘)) |
2 | 1 | exbidv 1925 |
. . . 4
β’ (π = πΊ β (βπ‘ π:(π‘ Γ π‘)βΆπ‘ β βπ‘ πΊ:(π‘ Γ π‘)βΆπ‘)) |
3 | | df-mgmOLD 36717 |
. . . 4
β’ Magma =
{π β£ βπ‘ π:(π‘ Γ π‘)βΆπ‘} |
4 | 2, 3 | elab2g 3671 |
. . 3
β’ (πΊ β π΄ β (πΊ β Magma β βπ‘ πΊ:(π‘ Γ π‘)βΆπ‘)) |
5 | | f00 6774 |
. . . . . . . 8
β’ (πΊ:(β
Γ
β
)βΆβ
β (πΊ = β
β§ (β
Γ β
) =
β
)) |
6 | | dmeq 5904 |
. . . . . . . . . 10
β’ (πΊ = β
β dom πΊ = dom β
) |
7 | | dmeq 5904 |
. . . . . . . . . . 11
β’ (dom
πΊ = dom β
β dom
dom πΊ = dom dom
β
) |
8 | | dm0 5921 |
. . . . . . . . . . . . 13
β’ dom
β
= β
|
9 | 8 | dmeqi 5905 |
. . . . . . . . . . . 12
β’ dom dom
β
= dom β
|
10 | 9, 8 | eqtri 2761 |
. . . . . . . . . . 11
β’ dom dom
β
= β
|
11 | 7, 10 | eqtr2di 2790 |
. . . . . . . . . 10
β’ (dom
πΊ = dom β
β
β
= dom dom πΊ) |
12 | 6, 11 | syl 17 |
. . . . . . . . 9
β’ (πΊ = β
β β
= dom
dom πΊ) |
13 | 12 | adantr 482 |
. . . . . . . 8
β’ ((πΊ = β
β§ (β
Γ β
) = β
) β β
= dom dom πΊ) |
14 | 5, 13 | sylbi 216 |
. . . . . . 7
β’ (πΊ:(β
Γ
β
)βΆβ
β β
= dom dom πΊ) |
15 | | xpeq12 5702 |
. . . . . . . . . 10
β’ ((π‘ = β
β§ π‘ = β
) β (π‘ Γ π‘) = (β
Γ
β
)) |
16 | 15 | anidms 568 |
. . . . . . . . 9
β’ (π‘ = β
β (π‘ Γ π‘) = (β
Γ
β
)) |
17 | | feq23 6702 |
. . . . . . . . 9
β’ (((π‘ Γ π‘) = (β
Γ β
) β§ π‘ = β
) β (πΊ:(π‘ Γ π‘)βΆπ‘ β πΊ:(β
Γ
β
)βΆβ
)) |
18 | 16, 17 | mpancom 687 |
. . . . . . . 8
β’ (π‘ = β
β (πΊ:(π‘ Γ π‘)βΆπ‘ β πΊ:(β
Γ
β
)βΆβ
)) |
19 | | eqeq1 2737 |
. . . . . . . 8
β’ (π‘ = β
β (π‘ = dom dom πΊ β β
= dom dom πΊ)) |
20 | 18, 19 | imbi12d 345 |
. . . . . . 7
β’ (π‘ = β
β ((πΊ:(π‘ Γ π‘)βΆπ‘ β π‘ = dom dom πΊ) β (πΊ:(β
Γ β
)βΆβ
β β
= dom dom πΊ))) |
21 | 14, 20 | mpbiri 258 |
. . . . . 6
β’ (π‘ = β
β (πΊ:(π‘ Γ π‘)βΆπ‘ β π‘ = dom dom πΊ)) |
22 | | fdm 6727 |
. . . . . . . 8
β’ (πΊ:(π‘ Γ π‘)βΆπ‘ β dom πΊ = (π‘ Γ π‘)) |
23 | | dmeq 5904 |
. . . . . . . 8
β’ (dom
πΊ = (π‘ Γ π‘) β dom dom πΊ = dom (π‘ Γ π‘)) |
24 | | df-ne 2942 |
. . . . . . . . . . . 12
β’ (π‘ β β
β Β¬ π‘ = β
) |
25 | | dmxp 5929 |
. . . . . . . . . . . 12
β’ (π‘ β β
β dom (π‘ Γ π‘) = π‘) |
26 | 24, 25 | sylbir 234 |
. . . . . . . . . . 11
β’ (Β¬
π‘ = β
β dom
(π‘ Γ π‘) = π‘) |
27 | 26 | eqeq1d 2735 |
. . . . . . . . . 10
β’ (Β¬
π‘ = β
β (dom
(π‘ Γ π‘) = dom dom πΊ β π‘ = dom dom πΊ)) |
28 | 27 | biimpcd 248 |
. . . . . . . . 9
β’ (dom
(π‘ Γ π‘) = dom dom πΊ β (Β¬ π‘ = β
β π‘ = dom dom πΊ)) |
29 | 28 | eqcoms 2741 |
. . . . . . . 8
β’ (dom dom
πΊ = dom (π‘ Γ π‘) β (Β¬ π‘ = β
β π‘ = dom dom πΊ)) |
30 | 22, 23, 29 | 3syl 18 |
. . . . . . 7
β’ (πΊ:(π‘ Γ π‘)βΆπ‘ β (Β¬ π‘ = β
β π‘ = dom dom πΊ)) |
31 | 30 | com12 32 |
. . . . . 6
β’ (Β¬
π‘ = β
β (πΊ:(π‘ Γ π‘)βΆπ‘ β π‘ = dom dom πΊ)) |
32 | 21, 31 | pm2.61i 182 |
. . . . 5
β’ (πΊ:(π‘ Γ π‘)βΆπ‘ β π‘ = dom dom πΊ) |
33 | 32 | pm4.71ri 562 |
. . . 4
β’ (πΊ:(π‘ Γ π‘)βΆπ‘ β (π‘ = dom dom πΊ β§ πΊ:(π‘ Γ π‘)βΆπ‘)) |
34 | 33 | exbii 1851 |
. . 3
β’
(βπ‘ πΊ:(π‘ Γ π‘)βΆπ‘ β βπ‘(π‘ = dom dom πΊ β§ πΊ:(π‘ Γ π‘)βΆπ‘)) |
35 | 4, 34 | bitrdi 287 |
. 2
β’ (πΊ β π΄ β (πΊ β Magma β βπ‘(π‘ = dom dom πΊ β§ πΊ:(π‘ Γ π‘)βΆπ‘))) |
36 | | dmexg 7894 |
. . 3
β’ (πΊ β π΄ β dom πΊ β V) |
37 | | dmexg 7894 |
. . 3
β’ (dom
πΊ β V β dom dom
πΊ β
V) |
38 | | xpeq12 5702 |
. . . . . . 7
β’ ((π‘ = dom dom πΊ β§ π‘ = dom dom πΊ) β (π‘ Γ π‘) = (dom dom πΊ Γ dom dom πΊ)) |
39 | 38 | anidms 568 |
. . . . . 6
β’ (π‘ = dom dom πΊ β (π‘ Γ π‘) = (dom dom πΊ Γ dom dom πΊ)) |
40 | | feq23 6702 |
. . . . . 6
β’ (((π‘ Γ π‘) = (dom dom πΊ Γ dom dom πΊ) β§ π‘ = dom dom πΊ) β (πΊ:(π‘ Γ π‘)βΆπ‘ β πΊ:(dom dom πΊ Γ dom dom πΊ)βΆdom dom πΊ)) |
41 | 39, 40 | mpancom 687 |
. . . . 5
β’ (π‘ = dom dom πΊ β (πΊ:(π‘ Γ π‘)βΆπ‘ β πΊ:(dom dom πΊ Γ dom dom πΊ)βΆdom dom πΊ)) |
42 | | ismgmOLD.1 |
. . . . . . . 8
β’ π = dom dom πΊ |
43 | 42 | eqcomi 2742 |
. . . . . . 7
β’ dom dom
πΊ = π |
44 | 43, 43 | xpeq12i 5705 |
. . . . . 6
β’ (dom dom
πΊ Γ dom dom πΊ) = (π Γ π) |
45 | 44, 43 | feq23i 6712 |
. . . . 5
β’ (πΊ:(dom dom πΊ Γ dom dom πΊ)βΆdom dom πΊ β πΊ:(π Γ π)βΆπ) |
46 | 41, 45 | bitrdi 287 |
. . . 4
β’ (π‘ = dom dom πΊ β (πΊ:(π‘ Γ π‘)βΆπ‘ β πΊ:(π Γ π)βΆπ)) |
47 | 46 | ceqsexgv 3643 |
. . 3
β’ (dom dom
πΊ β V β
(βπ‘(π‘ = dom dom πΊ β§ πΊ:(π‘ Γ π‘)βΆπ‘) β πΊ:(π Γ π)βΆπ)) |
48 | 36, 37, 47 | 3syl 18 |
. 2
β’ (πΊ β π΄ β (βπ‘(π‘ = dom dom πΊ β§ πΊ:(π‘ Γ π‘)βΆπ‘) β πΊ:(π Γ π)βΆπ)) |
49 | 35, 48 | bitrd 279 |
1
β’ (πΊ β π΄ β (πΊ β Magma β πΊ:(π Γ π)βΆπ)) |