Step |
Hyp |
Ref |
Expression |
1 |
|
isexid2.1 |
|- X = ran G |
2 |
|
rngopidOLD |
|- ( G e. ( Magma i^i ExId ) -> ran G = dom dom G ) |
3 |
|
elin |
|- ( G e. ( Magma i^i ExId ) <-> ( G e. Magma /\ G e. ExId ) ) |
4 |
|
eqid |
|- dom dom G = dom dom G |
5 |
4
|
isexid |
|- ( G e. ExId -> ( G e. ExId <-> E. u e. dom dom G A. x e. dom dom G ( ( u G x ) = x /\ ( x G u ) = x ) ) ) |
6 |
5
|
ibi |
|- ( G e. ExId -> E. u e. dom dom G A. x e. dom dom G ( ( u G x ) = x /\ ( x G u ) = x ) ) |
7 |
6
|
a1d |
|- ( G e. ExId -> ( X = dom dom G -> E. u e. dom dom G A. x e. dom dom G ( ( u G x ) = x /\ ( x G u ) = x ) ) ) |
8 |
7
|
adantl |
|- ( ( G e. Magma /\ G e. ExId ) -> ( X = dom dom G -> E. u e. dom dom G A. x e. dom dom G ( ( u G x ) = x /\ ( x G u ) = x ) ) ) |
9 |
3 8
|
sylbi |
|- ( G e. ( Magma i^i ExId ) -> ( X = dom dom G -> E. u e. dom dom G A. x e. dom dom G ( ( u G x ) = x /\ ( x G u ) = x ) ) ) |
10 |
|
eqeq2 |
|- ( ran G = dom dom G -> ( X = ran G <-> X = dom dom G ) ) |
11 |
|
raleq |
|- ( ran G = dom dom G -> ( A. x e. ran G ( ( u G x ) = x /\ ( x G u ) = x ) <-> A. x e. dom dom G ( ( u G x ) = x /\ ( x G u ) = x ) ) ) |
12 |
11
|
rexeqbi1dv |
|- ( ran G = dom dom G -> ( E. u e. ran G A. x e. ran G ( ( u G x ) = x /\ ( x G u ) = x ) <-> E. u e. dom dom G A. x e. dom dom G ( ( u G x ) = x /\ ( x G u ) = x ) ) ) |
13 |
10 12
|
imbi12d |
|- ( ran G = dom dom G -> ( ( X = ran G -> E. u e. ran G A. x e. ran G ( ( u G x ) = x /\ ( x G u ) = x ) ) <-> ( X = dom dom G -> E. u e. dom dom G A. x e. dom dom G ( ( u G x ) = x /\ ( x G u ) = x ) ) ) ) |
14 |
9 13
|
syl5ibr |
|- ( ran G = dom dom G -> ( G e. ( Magma i^i ExId ) -> ( X = ran G -> E. u e. ran G A. x e. ran G ( ( u G x ) = x /\ ( x G u ) = x ) ) ) ) |
15 |
2 14
|
mpcom |
|- ( G e. ( Magma i^i ExId ) -> ( X = ran G -> E. u e. ran G A. x e. ran G ( ( u G x ) = x /\ ( x G u ) = x ) ) ) |
16 |
15
|
com12 |
|- ( X = ran G -> ( G e. ( Magma i^i ExId ) -> E. u e. ran G A. x e. ran G ( ( u G x ) = x /\ ( x G u ) = x ) ) ) |
17 |
|
raleq |
|- ( X = ran G -> ( A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) <-> A. x e. ran G ( ( u G x ) = x /\ ( x G u ) = x ) ) ) |
18 |
17
|
rexeqbi1dv |
|- ( X = ran G -> ( E. u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) <-> E. u e. ran G A. x e. ran G ( ( u G x ) = x /\ ( x G u ) = x ) ) ) |
19 |
16 18
|
sylibrd |
|- ( X = ran G -> ( G e. ( Magma i^i ExId ) -> E. u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) ) |
20 |
1 19
|
ax-mp |
|- ( G e. ( Magma i^i ExId ) -> E. u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) |