Step |
Hyp |
Ref |
Expression |
1 |
|
ismgmOLD.1 |
|- X = dom dom G |
2 |
|
feq1 |
|- ( g = G -> ( g : ( t X. t ) --> t <-> G : ( t X. t ) --> t ) ) |
3 |
2
|
exbidv |
|- ( g = G -> ( E. t g : ( t X. t ) --> t <-> E. t G : ( t X. t ) --> t ) ) |
4 |
|
df-mgmOLD |
|- Magma = { g | E. t g : ( t X. t ) --> t } |
5 |
3 4
|
elab2g |
|- ( G e. A -> ( G e. Magma <-> E. t G : ( t X. t ) --> t ) ) |
6 |
|
f00 |
|- ( G : ( (/) X. (/) ) --> (/) <-> ( G = (/) /\ ( (/) X. (/) ) = (/) ) ) |
7 |
|
dmeq |
|- ( G = (/) -> dom G = dom (/) ) |
8 |
|
dmeq |
|- ( dom G = dom (/) -> dom dom G = dom dom (/) ) |
9 |
|
dm0 |
|- dom (/) = (/) |
10 |
9
|
dmeqi |
|- dom dom (/) = dom (/) |
11 |
10 9
|
eqtri |
|- dom dom (/) = (/) |
12 |
8 11
|
eqtr2di |
|- ( dom G = dom (/) -> (/) = dom dom G ) |
13 |
7 12
|
syl |
|- ( G = (/) -> (/) = dom dom G ) |
14 |
13
|
adantr |
|- ( ( G = (/) /\ ( (/) X. (/) ) = (/) ) -> (/) = dom dom G ) |
15 |
6 14
|
sylbi |
|- ( G : ( (/) X. (/) ) --> (/) -> (/) = dom dom G ) |
16 |
|
xpeq12 |
|- ( ( t = (/) /\ t = (/) ) -> ( t X. t ) = ( (/) X. (/) ) ) |
17 |
16
|
anidms |
|- ( t = (/) -> ( t X. t ) = ( (/) X. (/) ) ) |
18 |
|
feq23 |
|- ( ( ( t X. t ) = ( (/) X. (/) ) /\ t = (/) ) -> ( G : ( t X. t ) --> t <-> G : ( (/) X. (/) ) --> (/) ) ) |
19 |
17 18
|
mpancom |
|- ( t = (/) -> ( G : ( t X. t ) --> t <-> G : ( (/) X. (/) ) --> (/) ) ) |
20 |
|
eqeq1 |
|- ( t = (/) -> ( t = dom dom G <-> (/) = dom dom G ) ) |
21 |
19 20
|
imbi12d |
|- ( t = (/) -> ( ( G : ( t X. t ) --> t -> t = dom dom G ) <-> ( G : ( (/) X. (/) ) --> (/) -> (/) = dom dom G ) ) ) |
22 |
15 21
|
mpbiri |
|- ( t = (/) -> ( G : ( t X. t ) --> t -> t = dom dom G ) ) |
23 |
|
fdm |
|- ( G : ( t X. t ) --> t -> dom G = ( t X. t ) ) |
24 |
|
dmeq |
|- ( dom G = ( t X. t ) -> dom dom G = dom ( t X. t ) ) |
25 |
|
df-ne |
|- ( t =/= (/) <-> -. t = (/) ) |
26 |
|
dmxp |
|- ( t =/= (/) -> dom ( t X. t ) = t ) |
27 |
25 26
|
sylbir |
|- ( -. t = (/) -> dom ( t X. t ) = t ) |
28 |
27
|
eqeq1d |
|- ( -. t = (/) -> ( dom ( t X. t ) = dom dom G <-> t = dom dom G ) ) |
29 |
28
|
biimpcd |
|- ( dom ( t X. t ) = dom dom G -> ( -. t = (/) -> t = dom dom G ) ) |
30 |
29
|
eqcoms |
|- ( dom dom G = dom ( t X. t ) -> ( -. t = (/) -> t = dom dom G ) ) |
31 |
23 24 30
|
3syl |
|- ( G : ( t X. t ) --> t -> ( -. t = (/) -> t = dom dom G ) ) |
32 |
31
|
com12 |
|- ( -. t = (/) -> ( G : ( t X. t ) --> t -> t = dom dom G ) ) |
33 |
22 32
|
pm2.61i |
|- ( G : ( t X. t ) --> t -> t = dom dom G ) |
34 |
33
|
pm4.71ri |
|- ( G : ( t X. t ) --> t <-> ( t = dom dom G /\ G : ( t X. t ) --> t ) ) |
35 |
34
|
exbii |
|- ( E. t G : ( t X. t ) --> t <-> E. t ( t = dom dom G /\ G : ( t X. t ) --> t ) ) |
36 |
5 35
|
syl6bb |
|- ( G e. A -> ( G e. Magma <-> E. t ( t = dom dom G /\ G : ( t X. t ) --> t ) ) ) |
37 |
|
dmexg |
|- ( G e. A -> dom G e. _V ) |
38 |
|
dmexg |
|- ( dom G e. _V -> dom dom G e. _V ) |
39 |
|
xpeq12 |
|- ( ( t = dom dom G /\ t = dom dom G ) -> ( t X. t ) = ( dom dom G X. dom dom G ) ) |
40 |
39
|
anidms |
|- ( t = dom dom G -> ( t X. t ) = ( dom dom G X. dom dom G ) ) |
41 |
|
feq23 |
|- ( ( ( t X. t ) = ( dom dom G X. dom dom G ) /\ t = dom dom G ) -> ( G : ( t X. t ) --> t <-> G : ( dom dom G X. dom dom G ) --> dom dom G ) ) |
42 |
40 41
|
mpancom |
|- ( t = dom dom G -> ( G : ( t X. t ) --> t <-> G : ( dom dom G X. dom dom G ) --> dom dom G ) ) |
43 |
1
|
eqcomi |
|- dom dom G = X |
44 |
43 43
|
xpeq12i |
|- ( dom dom G X. dom dom G ) = ( X X. X ) |
45 |
44 43
|
feq23i |
|- ( G : ( dom dom G X. dom dom G ) --> dom dom G <-> G : ( X X. X ) --> X ) |
46 |
42 45
|
syl6bb |
|- ( t = dom dom G -> ( G : ( t X. t ) --> t <-> G : ( X X. X ) --> X ) ) |
47 |
46
|
ceqsexgv |
|- ( dom dom G e. _V -> ( E. t ( t = dom dom G /\ G : ( t X. t ) --> t ) <-> G : ( X X. X ) --> X ) ) |
48 |
37 38 47
|
3syl |
|- ( G e. A -> ( E. t ( t = dom dom G /\ G : ( t X. t ) --> t ) <-> G : ( X X. X ) --> X ) ) |
49 |
36 48
|
bitrd |
|- ( G e. A -> ( G e. Magma <-> G : ( X X. X ) --> X ) ) |