Step |
Hyp |
Ref |
Expression |
1 |
|
exidu1.1 |
|- X = ran G |
2 |
1
|
isexid2 |
|- ( G e. ( Magma i^i ExId ) -> E. u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) |
3 |
|
simpl |
|- ( ( ( u G x ) = x /\ ( x G u ) = x ) -> ( u G x ) = x ) |
4 |
3
|
ralimi |
|- ( A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) -> A. x e. X ( u G x ) = x ) |
5 |
|
oveq2 |
|- ( x = y -> ( u G x ) = ( u G y ) ) |
6 |
|
id |
|- ( x = y -> x = y ) |
7 |
5 6
|
eqeq12d |
|- ( x = y -> ( ( u G x ) = x <-> ( u G y ) = y ) ) |
8 |
7
|
rspcv |
|- ( y e. X -> ( A. x e. X ( u G x ) = x -> ( u G y ) = y ) ) |
9 |
4 8
|
syl5 |
|- ( y e. X -> ( A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) -> ( u G y ) = y ) ) |
10 |
|
simpr |
|- ( ( ( y G x ) = x /\ ( x G y ) = x ) -> ( x G y ) = x ) |
11 |
10
|
ralimi |
|- ( A. x e. X ( ( y G x ) = x /\ ( x G y ) = x ) -> A. x e. X ( x G y ) = x ) |
12 |
|
oveq1 |
|- ( x = u -> ( x G y ) = ( u G y ) ) |
13 |
|
id |
|- ( x = u -> x = u ) |
14 |
12 13
|
eqeq12d |
|- ( x = u -> ( ( x G y ) = x <-> ( u G y ) = u ) ) |
15 |
14
|
rspcv |
|- ( u e. X -> ( A. x e. X ( x G y ) = x -> ( u G y ) = u ) ) |
16 |
11 15
|
syl5 |
|- ( u e. X -> ( A. x e. X ( ( y G x ) = x /\ ( x G y ) = x ) -> ( u G y ) = u ) ) |
17 |
9 16
|
im2anan9r |
|- ( ( u e. X /\ y e. X ) -> ( ( A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) /\ A. x e. X ( ( y G x ) = x /\ ( x G y ) = x ) ) -> ( ( u G y ) = y /\ ( u G y ) = u ) ) ) |
18 |
|
eqtr2 |
|- ( ( ( u G y ) = y /\ ( u G y ) = u ) -> y = u ) |
19 |
18
|
equcomd |
|- ( ( ( u G y ) = y /\ ( u G y ) = u ) -> u = y ) |
20 |
17 19
|
syl6 |
|- ( ( u e. X /\ y e. X ) -> ( ( A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) /\ A. x e. X ( ( y G x ) = x /\ ( x G y ) = x ) ) -> u = y ) ) |
21 |
20
|
rgen2 |
|- A. u e. X A. y e. X ( ( A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) /\ A. x e. X ( ( y G x ) = x /\ ( x G y ) = x ) ) -> u = y ) |
22 |
|
oveq1 |
|- ( u = y -> ( u G x ) = ( y G x ) ) |
23 |
22
|
eqeq1d |
|- ( u = y -> ( ( u G x ) = x <-> ( y G x ) = x ) ) |
24 |
23
|
ovanraleqv |
|- ( u = y -> ( A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) <-> A. x e. X ( ( y G x ) = x /\ ( x G y ) = x ) ) ) |
25 |
24
|
reu4 |
|- ( E! u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) <-> ( E. u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) /\ A. u e. X A. y e. X ( ( A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) /\ A. x e. X ( ( y G x ) = x /\ ( x G y ) = x ) ) -> u = y ) ) ) |
26 |
2 21 25
|
sylanblrc |
|- ( G e. ( Magma i^i ExId ) -> E! u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) |