Step |
Hyp |
Ref |
Expression |
1 |
|
exidres.1 |
|- X = ran G |
2 |
|
exidres.2 |
|- U = ( GId ` G ) |
3 |
|
exidres.3 |
|- H = ( G |` ( Y X. Y ) ) |
4 |
1 2 3
|
exidreslem |
|- ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) -> ( U e. dom dom H /\ A. x e. dom dom H ( ( U H x ) = x /\ ( x H U ) = x ) ) ) |
5 |
|
oveq1 |
|- ( u = U -> ( u H x ) = ( U H x ) ) |
6 |
5
|
eqeq1d |
|- ( u = U -> ( ( u H x ) = x <-> ( U H x ) = x ) ) |
7 |
6
|
ovanraleqv |
|- ( u = U -> ( A. x e. dom dom H ( ( u H x ) = x /\ ( x H u ) = x ) <-> A. x e. dom dom H ( ( U H x ) = x /\ ( x H U ) = x ) ) ) |
8 |
7
|
rspcev |
|- ( ( U e. dom dom H /\ A. x e. dom dom H ( ( U H x ) = x /\ ( x H U ) = x ) ) -> E. u e. dom dom H A. x e. dom dom H ( ( u H x ) = x /\ ( x H u ) = x ) ) |
9 |
4 8
|
syl |
|- ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) -> E. u e. dom dom H A. x e. dom dom H ( ( u H x ) = x /\ ( x H u ) = x ) ) |
10 |
|
resexg |
|- ( G e. ( Magma i^i ExId ) -> ( G |` ( Y X. Y ) ) e. _V ) |
11 |
3 10
|
eqeltrid |
|- ( G e. ( Magma i^i ExId ) -> H e. _V ) |
12 |
|
eqid |
|- dom dom H = dom dom H |
13 |
12
|
isexid |
|- ( H e. _V -> ( H e. ExId <-> E. u e. dom dom H A. x e. dom dom H ( ( u H x ) = x /\ ( x H u ) = x ) ) ) |
14 |
11 13
|
syl |
|- ( G e. ( Magma i^i ExId ) -> ( H e. ExId <-> E. u e. dom dom H A. x e. dom dom H ( ( u H x ) = x /\ ( x H u ) = x ) ) ) |
15 |
14
|
3ad2ant1 |
|- ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) -> ( H e. ExId <-> E. u e. dom dom H A. x e. dom dom H ( ( u H x ) = x /\ ( x H u ) = x ) ) ) |
16 |
9 15
|
mpbird |
|- ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) -> H e. ExId ) |