Metamath Proof Explorer

Theorem isomuspgrlem2c

Description: Lemma 3 for isomuspgrlem2 . (Contributed by AV, 29-Nov-2022)

Ref Expression
Hypotheses isomushgr.v 
|- V = ( Vtx ` A )
isomushgr.w 
|- W = ( Vtx ` B )
isomushgr.e 
|- E = ( Edg ` A )
isomushgr.k 
|- K = ( Edg ` B )
isomuspgrlem2.g 
|- G = ( x e. E |-> ( F " x ) )
isomuspgrlem2.a 
|- ( ph -> A e. USPGraph )
isomuspgrlem2.f 
|- ( ph -> F : V -1-1-onto-> W )
isomuspgrlem2.i 
|- ( ph -> A. a e. V A. b e. V ( { a , b } e. E <-> { ( F ` a ) , ( F ` b ) } e. K ) )
isomuspgrlem2.x 
|- ( ph -> F e. X )
Assertion isomuspgrlem2c 
|- ( ph -> G : E -1-1-> K )

Proof

Step Hyp Ref Expression
1 isomushgr.v 
 |-  V = ( Vtx ` A )
2 isomushgr.w 
 |-  W = ( Vtx ` B )
3 isomushgr.e 
 |-  E = ( Edg ` A )
4 isomushgr.k 
 |-  K = ( Edg ` B )
5 isomuspgrlem2.g 
 |-  G = ( x e. E |-> ( F " x ) )
6 isomuspgrlem2.a 
 |-  ( ph -> A e. USPGraph )
7 isomuspgrlem2.f 
 |-  ( ph -> F : V -1-1-onto-> W )
8 isomuspgrlem2.i 
 |-  ( ph -> A. a e. V A. b e. V ( { a , b } e. E <-> { ( F ` a ) , ( F ` b ) } e. K ) )
9 isomuspgrlem2.x 
 |-  ( ph -> F e. X )
10 1 2 3 4 5 6 7 8 isomuspgrlem2b 
 |-  ( ph -> G : E --> K )
11 1 2 3 4 5 isomuspgrlem2a 
 |-  ( F e. X -> A. e e. E ( F " e ) = ( G ` e ) )
12 9 11 syl 
 |-  ( ph -> A. e e. E ( F " e ) = ( G ` e ) )
13 imaeq2 
 |-  ( e = c -> ( F " e ) = ( F " c ) )
14 fveq2 
 |-  ( e = c -> ( G ` e ) = ( G ` c ) )
15 13 14 eqeq12d 
 |-  ( e = c -> ( ( F " e ) = ( G ` e ) <-> ( F " c ) = ( G ` c ) ) )
16 15 rspcv 
 |-  ( c e. E -> ( A. e e. E ( F " e ) = ( G ` e ) -> ( F " c ) = ( G ` c ) ) )
17 16 ad2antrl 
 |-  ( ( ph /\ ( c e. E /\ d e. E ) ) -> ( A. e e. E ( F " e ) = ( G ` e ) -> ( F " c ) = ( G ` c ) ) )
18 17 imp 
 |-  ( ( ( ph /\ ( c e. E /\ d e. E ) ) /\ A. e e. E ( F " e ) = ( G ` e ) ) -> ( F " c ) = ( G ` c ) )
19 18 eqcomd 
 |-  ( ( ( ph /\ ( c e. E /\ d e. E ) ) /\ A. e e. E ( F " e ) = ( G ` e ) ) -> ( G ` c ) = ( F " c ) )
20 imaeq2 
 |-  ( e = d -> ( F " e ) = ( F " d ) )
21 fveq2 
 |-  ( e = d -> ( G ` e ) = ( G ` d ) )
22 20 21 eqeq12d 
 |-  ( e = d -> ( ( F " e ) = ( G ` e ) <-> ( F " d ) = ( G ` d ) ) )
23 22 rspcv 
 |-  ( d e. E -> ( A. e e. E ( F " e ) = ( G ` e ) -> ( F " d ) = ( G ` d ) ) )
24 23 ad2antll 
 |-  ( ( ph /\ ( c e. E /\ d e. E ) ) -> ( A. e e. E ( F " e ) = ( G ` e ) -> ( F " d ) = ( G ` d ) ) )
25 24 imp 
 |-  ( ( ( ph /\ ( c e. E /\ d e. E ) ) /\ A. e e. E ( F " e ) = ( G ` e ) ) -> ( F " d ) = ( G ` d ) )
26 25 eqcomd 
 |-  ( ( ( ph /\ ( c e. E /\ d e. E ) ) /\ A. e e. E ( F " e ) = ( G ` e ) ) -> ( G ` d ) = ( F " d ) )
27 19 26 eqeq12d 
 |-  ( ( ( ph /\ ( c e. E /\ d e. E ) ) /\ A. e e. E ( F " e ) = ( G ` e ) ) -> ( ( G ` c ) = ( G ` d ) <-> ( F " c ) = ( F " d ) ) )
28 12 27 mpidan 
 |-  ( ( ph /\ ( c e. E /\ d e. E ) ) -> ( ( G ` c ) = ( G ` d ) <-> ( F " c ) = ( F " d ) ) )
29 f1of1 
 |-  ( F : V -1-1-onto-> W -> F : V -1-1-> W )
30 7 29 syl 
 |-  ( ph -> F : V -1-1-> W )
31 uspgrupgr 
 |-  ( A e. USPGraph -> A e. UPGraph )
32 upgruhgr 
 |-  ( A e. UPGraph -> A e. UHGraph )
33 3 eleq2i 
 |-  ( c e. E <-> c e. ( Edg ` A ) )
34 edguhgr 
 |-  ( ( A e. UHGraph /\ c e. ( Edg ` A ) ) -> c e. ~P ( Vtx ` A ) )
35 elpwi 
 |-  ( c e. ~P ( Vtx ` A ) -> c C_ ( Vtx ` A ) )
36 35 1 sseqtrrdi 
 |-  ( c e. ~P ( Vtx ` A ) -> c C_ V )
37 34 36 syl 
 |-  ( ( A e. UHGraph /\ c e. ( Edg ` A ) ) -> c C_ V )
38 37 ex 
 |-  ( A e. UHGraph -> ( c e. ( Edg ` A ) -> c C_ V ) )
39 33 38 syl5bi 
 |-  ( A e. UHGraph -> ( c e. E -> c C_ V ) )
40 3 eleq2i 
 |-  ( d e. E <-> d e. ( Edg ` A ) )
41 edguhgr 
 |-  ( ( A e. UHGraph /\ d e. ( Edg ` A ) ) -> d e. ~P ( Vtx ` A ) )
42 elpwi 
 |-  ( d e. ~P ( Vtx ` A ) -> d C_ ( Vtx ` A ) )
43 42 1 sseqtrrdi 
 |-  ( d e. ~P ( Vtx ` A ) -> d C_ V )
44 41 43 syl 
 |-  ( ( A e. UHGraph /\ d e. ( Edg ` A ) ) -> d C_ V )
45 44 ex 
 |-  ( A e. UHGraph -> ( d e. ( Edg ` A ) -> d C_ V ) )
46 40 45 syl5bi 
 |-  ( A e. UHGraph -> ( d e. E -> d C_ V ) )
47 39 46 anim12d 
 |-  ( A e. UHGraph -> ( ( c e. E /\ d e. E ) -> ( c C_ V /\ d C_ V ) ) )
48 32 47 syl 
 |-  ( A e. UPGraph -> ( ( c e. E /\ d e. E ) -> ( c C_ V /\ d C_ V ) ) )
49 6 31 48 3syl 
 |-  ( ph -> ( ( c e. E /\ d e. E ) -> ( c C_ V /\ d C_ V ) ) )
50 49 imp 
 |-  ( ( ph /\ ( c e. E /\ d e. E ) ) -> ( c C_ V /\ d C_ V ) )
51 f1imaeq 
 |-  ( ( F : V -1-1-> W /\ ( c C_ V /\ d C_ V ) ) -> ( ( F " c ) = ( F " d ) <-> c = d ) )
52 30 50 51 syl2an2r 
 |-  ( ( ph /\ ( c e. E /\ d e. E ) ) -> ( ( F " c ) = ( F " d ) <-> c = d ) )
53 52 biimpd 
 |-  ( ( ph /\ ( c e. E /\ d e. E ) ) -> ( ( F " c ) = ( F " d ) -> c = d ) )
54 28 53 sylbid 
 |-  ( ( ph /\ ( c e. E /\ d e. E ) ) -> ( ( G ` c ) = ( G ` d ) -> c = d ) )
55 54 ralrimivva 
 |-  ( ph -> A. c e. E A. d e. E ( ( G ` c ) = ( G ` d ) -> c = d ) )
56 dff13 
 |-  ( G : E -1-1-> K <-> ( G : E --> K /\ A. c e. E A. d e. E ( ( G ` c ) = ( G ` d ) -> c = d ) ) )
57 10 55 56 sylanbrc 
 |-  ( ph -> G : E -1-1-> K )