Metamath Proof Explorer

Theorem isomuspgrlem2b

Description: Lemma 2 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 ) )
Assertion isomuspgrlem2b 
|- ( ph -> G : E --> 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 uspgrupgr 
 |-  ( A e. USPGraph -> A e. UPGraph )
10 6 9 syl 
 |-  ( ph -> A e. UPGraph )
11 1 3 upgredg 
 |-  ( ( A e. UPGraph /\ x e. E ) -> E. c e. V E. d e. V x = { c , d } )
12 10 11 sylan 
 |-  ( ( ph /\ x e. E ) -> E. c e. V E. d e. V x = { c , d } )
13 preq12 
 |-  ( ( a = c /\ b = d ) -> { a , b } = { c , d } )
14 13 eleq1d 
 |-  ( ( a = c /\ b = d ) -> ( { a , b } e. E <-> { c , d } e. E ) )
15 fveq2 
 |-  ( a = c -> ( F ` a ) = ( F ` c ) )
16 15 adantr 
 |-  ( ( a = c /\ b = d ) -> ( F ` a ) = ( F ` c ) )
17 fveq2 
 |-  ( b = d -> ( F ` b ) = ( F ` d ) )
18 17 adantl 
 |-  ( ( a = c /\ b = d ) -> ( F ` b ) = ( F ` d ) )
19 16 18 preq12d 
 |-  ( ( a = c /\ b = d ) -> { ( F ` a ) , ( F ` b ) } = { ( F ` c ) , ( F ` d ) } )
20 19 eleq1d 
 |-  ( ( a = c /\ b = d ) -> ( { ( F ` a ) , ( F ` b ) } e. K <-> { ( F ` c ) , ( F ` d ) } e. K ) )
21 14 20 bibi12d 
 |-  ( ( a = c /\ b = d ) -> ( ( { a , b } e. E <-> { ( F ` a ) , ( F ` b ) } e. K ) <-> ( { c , d } e. E <-> { ( F ` c ) , ( F ` d ) } e. K ) ) )
22 21 rspc2gv 
 |-  ( ( c e. V /\ d e. V ) -> ( A. a e. V A. b e. V ( { a , b } e. E <-> { ( F ` a ) , ( F ` b ) } e. K ) -> ( { c , d } e. E <-> { ( F ` c ) , ( F ` d ) } e. K ) ) )
23 8 22 syl5com 
 |-  ( ph -> ( ( c e. V /\ d e. V ) -> ( { c , d } e. E <-> { ( F ` c ) , ( F ` d ) } e. K ) ) )
24 23 adantr 
 |-  ( ( ph /\ x = { c , d } ) -> ( ( c e. V /\ d e. V ) -> ( { c , d } e. E <-> { ( F ` c ) , ( F ` d ) } e. K ) ) )
25 24 imp 
 |-  ( ( ( ph /\ x = { c , d } ) /\ ( c e. V /\ d e. V ) ) -> ( { c , d } e. E <-> { ( F ` c ) , ( F ` d ) } e. K ) )
26 bicom 
 |-  ( ( { c , d } e. E <-> { ( F ` c ) , ( F ` d ) } e. K ) <-> ( { ( F ` c ) , ( F ` d ) } e. K <-> { c , d } e. E ) )
27 bianir 
 |-  ( ( { c , d } e. E /\ ( { ( F ` c ) , ( F ` d ) } e. K <-> { c , d } e. E ) ) -> { ( F ` c ) , ( F ` d ) } e. K )
28 27 ex 
 |-  ( { c , d } e. E -> ( ( { ( F ` c ) , ( F ` d ) } e. K <-> { c , d } e. E ) -> { ( F ` c ) , ( F ` d ) } e. K ) )
29 26 28 syl5bi 
 |-  ( { c , d } e. E -> ( ( { c , d } e. E <-> { ( F ` c ) , ( F ` d ) } e. K ) -> { ( F ` c ) , ( F ` d ) } e. K ) )
30 f1ofn 
 |-  ( F : V -1-1-onto-> W -> F Fn V )
31 7 30 syl 
 |-  ( ph -> F Fn V )
32 31 adantr 
 |-  ( ( ph /\ x = { c , d } ) -> F Fn V )
33 32 adantr 
 |-  ( ( ( ph /\ x = { c , d } ) /\ ( c e. V /\ d e. V ) ) -> F Fn V )
34 simprl 
 |-  ( ( ( ph /\ x = { c , d } ) /\ ( c e. V /\ d e. V ) ) -> c e. V )
35 simprr 
 |-  ( ( ( ph /\ x = { c , d } ) /\ ( c e. V /\ d e. V ) ) -> d e. V )
36 33 34 35 3jca 
 |-  ( ( ( ph /\ x = { c , d } ) /\ ( c e. V /\ d e. V ) ) -> ( F Fn V /\ c e. V /\ d e. V ) )
37 36 adantl 
 |-  ( ( { c , d } e. E /\ ( ( ph /\ x = { c , d } ) /\ ( c e. V /\ d e. V ) ) ) -> ( F Fn V /\ c e. V /\ d e. V ) )
38 fnimapr 
 |-  ( ( F Fn V /\ c e. V /\ d e. V ) -> ( F " { c , d } ) = { ( F ` c ) , ( F ` d ) } )
39 37 38 syl 
 |-  ( ( { c , d } e. E /\ ( ( ph /\ x = { c , d } ) /\ ( c e. V /\ d e. V ) ) ) -> ( F " { c , d } ) = { ( F ` c ) , ( F ` d ) } )
40 39 eqcomd 
 |-  ( ( { c , d } e. E /\ ( ( ph /\ x = { c , d } ) /\ ( c e. V /\ d e. V ) ) ) -> { ( F ` c ) , ( F ` d ) } = ( F " { c , d } ) )
41 40 eleq1d 
 |-  ( ( { c , d } e. E /\ ( ( ph /\ x = { c , d } ) /\ ( c e. V /\ d e. V ) ) ) -> ( { ( F ` c ) , ( F ` d ) } e. K <-> ( F " { c , d } ) e. K ) )
42 41 biimpd 
 |-  ( ( { c , d } e. E /\ ( ( ph /\ x = { c , d } ) /\ ( c e. V /\ d e. V ) ) ) -> ( { ( F ` c ) , ( F ` d ) } e. K -> ( F " { c , d } ) e. K ) )
43 42 ex 
 |-  ( { c , d } e. E -> ( ( ( ph /\ x = { c , d } ) /\ ( c e. V /\ d e. V ) ) -> ( { ( F ` c ) , ( F ` d ) } e. K -> ( F " { c , d } ) e. K ) ) )
44 43 com23 
 |-  ( { c , d } e. E -> ( { ( F ` c ) , ( F ` d ) } e. K -> ( ( ( ph /\ x = { c , d } ) /\ ( c e. V /\ d e. V ) ) -> ( F " { c , d } ) e. K ) ) )
45 29 44 syld 
 |-  ( { c , d } e. E -> ( ( { c , d } e. E <-> { ( F ` c ) , ( F ` d ) } e. K ) -> ( ( ( ph /\ x = { c , d } ) /\ ( c e. V /\ d e. V ) ) -> ( F " { c , d } ) e. K ) ) )
46 45 com13 
 |-  ( ( ( ph /\ x = { c , d } ) /\ ( c e. V /\ d e. V ) ) -> ( ( { c , d } e. E <-> { ( F ` c ) , ( F ` d ) } e. K ) -> ( { c , d } e. E -> ( F " { c , d } ) e. K ) ) )
47 25 46 mpd 
 |-  ( ( ( ph /\ x = { c , d } ) /\ ( c e. V /\ d e. V ) ) -> ( { c , d } e. E -> ( F " { c , d } ) e. K ) )
48 eleq1 
 |-  ( x = { c , d } -> ( x e. E <-> { c , d } e. E ) )
49 imaeq2 
 |-  ( x = { c , d } -> ( F " x ) = ( F " { c , d } ) )
50 49 eleq1d 
 |-  ( x = { c , d } -> ( ( F " x ) e. K <-> ( F " { c , d } ) e. K ) )
51 48 50 imbi12d 
 |-  ( x = { c , d } -> ( ( x e. E -> ( F " x ) e. K ) <-> ( { c , d } e. E -> ( F " { c , d } ) e. K ) ) )
52 51 adantl 
 |-  ( ( ph /\ x = { c , d } ) -> ( ( x e. E -> ( F " x ) e. K ) <-> ( { c , d } e. E -> ( F " { c , d } ) e. K ) ) )
53 52 adantr 
 |-  ( ( ( ph /\ x = { c , d } ) /\ ( c e. V /\ d e. V ) ) -> ( ( x e. E -> ( F " x ) e. K ) <-> ( { c , d } e. E -> ( F " { c , d } ) e. K ) ) )
54 47 53 mpbird 
 |-  ( ( ( ph /\ x = { c , d } ) /\ ( c e. V /\ d e. V ) ) -> ( x e. E -> ( F " x ) e. K ) )
55 54 exp31 
 |-  ( ph -> ( x = { c , d } -> ( ( c e. V /\ d e. V ) -> ( x e. E -> ( F " x ) e. K ) ) ) )
56 55 com24 
 |-  ( ph -> ( x e. E -> ( ( c e. V /\ d e. V ) -> ( x = { c , d } -> ( F " x ) e. K ) ) ) )
57 56 imp31 
 |-  ( ( ( ph /\ x e. E ) /\ ( c e. V /\ d e. V ) ) -> ( x = { c , d } -> ( F " x ) e. K ) )
58 57 rexlimdvva 
 |-  ( ( ph /\ x e. E ) -> ( E. c e. V E. d e. V x = { c , d } -> ( F " x ) e. K ) )
59 12 58 mpd 
 |-  ( ( ph /\ x e. E ) -> ( F " x ) e. K )
60 59 ralrimiva 
 |-  ( ph -> A. x e. E ( F " x ) e. K )
61 5 fmpt 
 |-  ( A. x e. E ( F " x ) e. K <-> G : E --> K )
62 60 61 sylib 
 |-  ( ph -> G : E --> K )