Metamath Proof Explorer

Theorem exidreslem

Description: Lemma for exidres and exidresid . (Contributed by Jeff Madsen, 8-Jun-2010) (Revised by Mario Carneiro, 23-Dec-2013)

Ref Expression
Hypotheses exidres.1 
|- X = ran G
exidres.2 
|- U = ( GId ` G )
exidres.3 
|- H = ( G |` ( Y X. Y ) )
Assertion 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 ) ) )

Proof

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 3 dmeqi 
 |-  dom H = dom ( G |` ( Y X. Y ) )
5 xpss12 
 |-  ( ( Y C_ X /\ Y C_ X ) -> ( Y X. Y ) C_ ( X X. X ) )
6 5 anidms 
 |-  ( Y C_ X -> ( Y X. Y ) C_ ( X X. X ) )
7 1 opidon2OLD 
 |-  ( G e. ( Magma i^i ExId ) -> G : ( X X. X ) -onto-> X )
8 fof 
 |-  ( G : ( X X. X ) -onto-> X -> G : ( X X. X ) --> X )
9 fdm 
 |-  ( G : ( X X. X ) --> X -> dom G = ( X X. X ) )
10 7 8 9 3syl 
 |-  ( G e. ( Magma i^i ExId ) -> dom G = ( X X. X ) )
11 10 sseq2d 
 |-  ( G e. ( Magma i^i ExId ) -> ( ( Y X. Y ) C_ dom G <-> ( Y X. Y ) C_ ( X X. X ) ) )
12 6 11 syl5ibr 
 |-  ( G e. ( Magma i^i ExId ) -> ( Y C_ X -> ( Y X. Y ) C_ dom G ) )
13 12 imp 
 |-  ( ( G e. ( Magma i^i ExId ) /\ Y C_ X ) -> ( Y X. Y ) C_ dom G )
14 ssdmres 
 |-  ( ( Y X. Y ) C_ dom G <-> dom ( G |` ( Y X. Y ) ) = ( Y X. Y ) )
15 13 14 sylib 
 |-  ( ( G e. ( Magma i^i ExId ) /\ Y C_ X ) -> dom ( G |` ( Y X. Y ) ) = ( Y X. Y ) )
16 4 15 syl5eq 
 |-  ( ( G e. ( Magma i^i ExId ) /\ Y C_ X ) -> dom H = ( Y X. Y ) )
17 16 dmeqd 
 |-  ( ( G e. ( Magma i^i ExId ) /\ Y C_ X ) -> dom dom H = dom ( Y X. Y ) )
18 dmxpid 
 |-  dom ( Y X. Y ) = Y
19 17 18 eqtrdi 
 |-  ( ( G e. ( Magma i^i ExId ) /\ Y C_ X ) -> dom dom H = Y )
20 19 eleq2d 
 |-  ( ( G e. ( Magma i^i ExId ) /\ Y C_ X ) -> ( U e. dom dom H <-> U e. Y ) )
21 20 biimp3ar 
 |-  ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) -> U e. dom dom H )
22 ssel2 
 |-  ( ( Y C_ X /\ x e. Y ) -> x e. X )
23 1 2 cmpidelt 
 |-  ( ( G e. ( Magma i^i ExId ) /\ x e. X ) -> ( ( U G x ) = x /\ ( x G U ) = x ) )
24 22 23 sylan2 
 |-  ( ( G e. ( Magma i^i ExId ) /\ ( Y C_ X /\ x e. Y ) ) -> ( ( U G x ) = x /\ ( x G U ) = x ) )
25 24 anassrs 
 |-  ( ( ( G e. ( Magma i^i ExId ) /\ Y C_ X ) /\ x e. Y ) -> ( ( U G x ) = x /\ ( x G U ) = x ) )
26 25 adantrl 
 |-  ( ( ( G e. ( Magma i^i ExId ) /\ Y C_ X ) /\ ( U e. Y /\ x e. Y ) ) -> ( ( U G x ) = x /\ ( x G U ) = x ) )
27 3 oveqi 
 |-  ( U H x ) = ( U ( G |` ( Y X. Y ) ) x )
28 ovres 
 |-  ( ( U e. Y /\ x e. Y ) -> ( U ( G |` ( Y X. Y ) ) x ) = ( U G x ) )
29 27 28 syl5eq 
 |-  ( ( U e. Y /\ x e. Y ) -> ( U H x ) = ( U G x ) )
30 29 eqeq1d 
 |-  ( ( U e. Y /\ x e. Y ) -> ( ( U H x ) = x <-> ( U G x ) = x ) )
31 3 oveqi 
 |-  ( x H U ) = ( x ( G |` ( Y X. Y ) ) U )
32 ovres 
 |-  ( ( x e. Y /\ U e. Y ) -> ( x ( G |` ( Y X. Y ) ) U ) = ( x G U ) )
33 31 32 syl5eq 
 |-  ( ( x e. Y /\ U e. Y ) -> ( x H U ) = ( x G U ) )
34 33 ancoms 
 |-  ( ( U e. Y /\ x e. Y ) -> ( x H U ) = ( x G U ) )
35 34 eqeq1d 
 |-  ( ( U e. Y /\ x e. Y ) -> ( ( x H U ) = x <-> ( x G U ) = x ) )
36 30 35 anbi12d 
 |-  ( ( U e. Y /\ x e. Y ) -> ( ( ( U H x ) = x /\ ( x H U ) = x ) <-> ( ( U G x ) = x /\ ( x G U ) = x ) ) )
37 36 adantl 
 |-  ( ( ( G e. ( Magma i^i ExId ) /\ Y C_ X ) /\ ( U e. Y /\ x e. Y ) ) -> ( ( ( U H x ) = x /\ ( x H U ) = x ) <-> ( ( U G x ) = x /\ ( x G U ) = x ) ) )
38 26 37 mpbird 
 |-  ( ( ( G e. ( Magma i^i ExId ) /\ Y C_ X ) /\ ( U e. Y /\ x e. Y ) ) -> ( ( U H x ) = x /\ ( x H U ) = x ) )
39 38 anassrs 
 |-  ( ( ( ( G e. ( Magma i^i ExId ) /\ Y C_ X ) /\ U e. Y ) /\ x e. Y ) -> ( ( U H x ) = x /\ ( x H U ) = x ) )
40 39 ralrimiva 
 |-  ( ( ( G e. ( Magma i^i ExId ) /\ Y C_ X ) /\ U e. Y ) -> A. x e. Y ( ( U H x ) = x /\ ( x H U ) = x ) )
41 40 3impa 
 |-  ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) -> A. x e. Y ( ( U H x ) = x /\ ( x H U ) = x ) )
42 13 3adant3 
 |-  ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) -> ( Y X. Y ) C_ dom G )
43 42 14 sylib 
 |-  ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) -> dom ( G |` ( Y X. Y ) ) = ( Y X. Y ) )
44 4 43 syl5eq 
 |-  ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) -> dom H = ( Y X. Y ) )
45 44 dmeqd 
 |-  ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) -> dom dom H = dom ( Y X. Y ) )
46 45 18 eqtrdi 
 |-  ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) -> dom dom H = Y )
47 46 raleqdv 
 |-  ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) -> ( A. x e. dom dom H ( ( U H x ) = x /\ ( x H U ) = x ) <-> A. x e. Y ( ( U H x ) = x /\ ( x H U ) = x ) ) )
48 41 47 mpbird 
 |-  ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) -> A. x e. dom dom H ( ( U H x ) = x /\ ( x H U ) = x ) )
49 21 48 jca 
 |-  ( ( 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 ) ) )