Metamath Proof Explorer

Theorem isomuspgrlem2d

Description: Lemma 4 for isomuspgrlem2 . (Contributed by AV, 1-Dec-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 )
isomuspgrlem2.b 
|- ( ph -> B e. USPGraph )
Assertion isomuspgrlem2d 
|- ( ph -> G : E -onto-> 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 isomuspgrlem2.b 
 |-  ( ph -> B e. USPGraph )
11 1 2 3 4 5 6 7 8 isomuspgrlem2b 
 |-  ( ph -> G : E --> K )
12 uspgrupgr 
 |-  ( B e. USPGraph -> B e. UPGraph )
13 10 12 syl 
 |-  ( ph -> B e. UPGraph )
14 2 4 upgredg 
 |-  ( ( B e. UPGraph /\ y e. K ) -> E. c e. W E. d e. W y = { c , d } )
15 13 14 sylan 
 |-  ( ( ph /\ y e. K ) -> E. c e. W E. d e. W y = { c , d } )
16 eleq1 
 |-  ( y = { c , d } -> ( y e. K <-> { c , d } e. K ) )
17 16 anbi2d 
 |-  ( y = { c , d } -> ( ( ph /\ y e. K ) <-> ( ph /\ { c , d } e. K ) ) )
18 f1ofo 
 |-  ( F : V -1-1-onto-> W -> F : V -onto-> W )
19 7 18 syl 
 |-  ( ph -> F : V -onto-> W )
20 foelrn 
 |-  ( ( F : V -onto-> W /\ c e. W ) -> E. m e. V c = ( F ` m ) )
21 19 20 sylan 
 |-  ( ( ph /\ c e. W ) -> E. m e. V c = ( F ` m ) )
22 21 ex 
 |-  ( ph -> ( c e. W -> E. m e. V c = ( F ` m ) ) )
23 foelrn 
 |-  ( ( F : V -onto-> W /\ d e. W ) -> E. n e. V d = ( F ` n ) )
24 19 23 sylan 
 |-  ( ( ph /\ d e. W ) -> E. n e. V d = ( F ` n ) )
25 24 ex 
 |-  ( ph -> ( d e. W -> E. n e. V d = ( F ` n ) ) )
26 22 25 anim12d 
 |-  ( ph -> ( ( c e. W /\ d e. W ) -> ( E. m e. V c = ( F ` m ) /\ E. n e. V d = ( F ` n ) ) ) )
27 26 adantr 
 |-  ( ( ph /\ { c , d } e. K ) -> ( ( c e. W /\ d e. W ) -> ( E. m e. V c = ( F ` m ) /\ E. n e. V d = ( F ` n ) ) ) )
28 27 imp 
 |-  ( ( ( ph /\ { c , d } e. K ) /\ ( c e. W /\ d e. W ) ) -> ( E. m e. V c = ( F ` m ) /\ E. n e. V d = ( F ` n ) ) )
29 preq12 
 |-  ( ( c = ( F ` m ) /\ d = ( F ` n ) ) -> { c , d } = { ( F ` m ) , ( F ` n ) } )
30 29 ancoms 
 |-  ( ( d = ( F ` n ) /\ c = ( F ` m ) ) -> { c , d } = { ( F ` m ) , ( F ` n ) } )
31 30 eleq1d 
 |-  ( ( d = ( F ` n ) /\ c = ( F ` m ) ) -> ( { c , d } e. K <-> { ( F ` m ) , ( F ` n ) } e. K ) )
32 preq1 
 |-  ( a = m -> { a , b } = { m , b } )
33 32 eleq1d 
 |-  ( a = m -> ( { a , b } e. E <-> { m , b } e. E ) )
34 fveq2 
 |-  ( a = m -> ( F ` a ) = ( F ` m ) )
35 34 preq1d 
 |-  ( a = m -> { ( F ` a ) , ( F ` b ) } = { ( F ` m ) , ( F ` b ) } )
36 35 eleq1d 
 |-  ( a = m -> ( { ( F ` a ) , ( F ` b ) } e. K <-> { ( F ` m ) , ( F ` b ) } e. K ) )
37 33 36 bibi12d 
 |-  ( a = m -> ( ( { a , b } e. E <-> { ( F ` a ) , ( F ` b ) } e. K ) <-> ( { m , b } e. E <-> { ( F ` m ) , ( F ` b ) } e. K ) ) )
38 preq2 
 |-  ( b = n -> { m , b } = { m , n } )
39 38 eleq1d 
 |-  ( b = n -> ( { m , b } e. E <-> { m , n } e. E ) )
40 fveq2 
 |-  ( b = n -> ( F ` b ) = ( F ` n ) )
41 40 preq2d 
 |-  ( b = n -> { ( F ` m ) , ( F ` b ) } = { ( F ` m ) , ( F ` n ) } )
42 41 eleq1d 
 |-  ( b = n -> ( { ( F ` m ) , ( F ` b ) } e. K <-> { ( F ` m ) , ( F ` n ) } e. K ) )
43 39 42 bibi12d 
 |-  ( b = n -> ( ( { m , b } e. E <-> { ( F ` m ) , ( F ` b ) } e. K ) <-> ( { m , n } e. E <-> { ( F ` m ) , ( F ` n ) } e. K ) ) )
44 37 43 rspc2va 
 |-  ( ( ( m e. V /\ n e. V ) /\ A. a e. V A. b e. V ( { a , b } e. E <-> { ( F ` a ) , ( F ` b ) } e. K ) ) -> ( { m , n } e. E <-> { ( F ` m ) , ( F ` n ) } e. K ) )
45 44 bicomd 
 |-  ( ( ( m e. V /\ n e. V ) /\ A. a e. V A. b e. V ( { a , b } e. E <-> { ( F ` a ) , ( F ` b ) } e. K ) ) -> ( { ( F ` m ) , ( F ` n ) } e. K <-> { m , n } e. E ) )
46 45 ancoms 
 |-  ( ( A. a e. V A. b e. V ( { a , b } e. E <-> { ( F ` a ) , ( F ` b ) } e. K ) /\ ( m e. V /\ n e. V ) ) -> ( { ( F ` m ) , ( F ` n ) } e. K <-> { m , n } e. E ) )
47 46 biimpd 
 |-  ( ( A. a e. V A. b e. V ( { a , b } e. E <-> { ( F ` a ) , ( F ` b ) } e. K ) /\ ( m e. V /\ n e. V ) ) -> ( { ( F ` m ) , ( F ` n ) } e. K -> { m , n } e. E ) )
48 47 ex 
 |-  ( A. a e. V A. b e. V ( { a , b } e. E <-> { ( F ` a ) , ( F ` b ) } e. K ) -> ( ( m e. V /\ n e. V ) -> ( { ( F ` m ) , ( F ` n ) } e. K -> { m , n } e. E ) ) )
49 8 48 syl 
 |-  ( ph -> ( ( m e. V /\ n e. V ) -> ( { ( F ` m ) , ( F ` n ) } e. K -> { m , n } e. E ) ) )
50 49 com13 
 |-  ( { ( F ` m ) , ( F ` n ) } e. K -> ( ( m e. V /\ n e. V ) -> ( ph -> { m , n } e. E ) ) )
51 31 50 syl6bi 
 |-  ( ( d = ( F ` n ) /\ c = ( F ` m ) ) -> ( { c , d } e. K -> ( ( m e. V /\ n e. V ) -> ( ph -> { m , n } e. E ) ) ) )
52 51 com14 
 |-  ( ph -> ( { c , d } e. K -> ( ( m e. V /\ n e. V ) -> ( ( d = ( F ` n ) /\ c = ( F ` m ) ) -> { m , n } e. E ) ) ) )
53 52 imp 
 |-  ( ( ph /\ { c , d } e. K ) -> ( ( m e. V /\ n e. V ) -> ( ( d = ( F ` n ) /\ c = ( F ` m ) ) -> { m , n } e. E ) ) )
54 53 adantr 
 |-  ( ( ( ph /\ { c , d } e. K ) /\ ( c e. W /\ d e. W ) ) -> ( ( m e. V /\ n e. V ) -> ( ( d = ( F ` n ) /\ c = ( F ` m ) ) -> { m , n } e. E ) ) )
55 54 imp31 
 |-  ( ( ( ( ( ph /\ { c , d } e. K ) /\ ( c e. W /\ d e. W ) ) /\ ( m e. V /\ n e. V ) ) /\ ( d = ( F ` n ) /\ c = ( F ` m ) ) ) -> { m , n } e. E )
56 imaeq2 
 |-  ( e = { m , n } -> ( F " e ) = ( F " { m , n } ) )
57 f1ofn 
 |-  ( F : V -1-1-onto-> W -> F Fn V )
58 7 57 syl 
 |-  ( ph -> F Fn V )
59 58 ad3antrrr 
 |-  ( ( ( ( ph /\ { c , d } e. K ) /\ ( c e. W /\ d e. W ) ) /\ ( m e. V /\ n e. V ) ) -> F Fn V )
60 simprl 
 |-  ( ( ( ( ph /\ { c , d } e. K ) /\ ( c e. W /\ d e. W ) ) /\ ( m e. V /\ n e. V ) ) -> m e. V )
61 simpr 
 |-  ( ( m e. V /\ n e. V ) -> n e. V )
62 61 adantl 
 |-  ( ( ( ( ph /\ { c , d } e. K ) /\ ( c e. W /\ d e. W ) ) /\ ( m e. V /\ n e. V ) ) -> n e. V )
63 59 60 62 3jca 
 |-  ( ( ( ( ph /\ { c , d } e. K ) /\ ( c e. W /\ d e. W ) ) /\ ( m e. V /\ n e. V ) ) -> ( F Fn V /\ m e. V /\ n e. V ) )
64 63 adantr 
 |-  ( ( ( ( ( ph /\ { c , d } e. K ) /\ ( c e. W /\ d e. W ) ) /\ ( m e. V /\ n e. V ) ) /\ ( d = ( F ` n ) /\ c = ( F ` m ) ) ) -> ( F Fn V /\ m e. V /\ n e. V ) )
65 fnimapr 
 |-  ( ( F Fn V /\ m e. V /\ n e. V ) -> ( F " { m , n } ) = { ( F ` m ) , ( F ` n ) } )
66 64 65 syl 
 |-  ( ( ( ( ( ph /\ { c , d } e. K ) /\ ( c e. W /\ d e. W ) ) /\ ( m e. V /\ n e. V ) ) /\ ( d = ( F ` n ) /\ c = ( F ` m ) ) ) -> ( F " { m , n } ) = { ( F ` m ) , ( F ` n ) } )
67 56 66 sylan9eqr 
 |-  ( ( ( ( ( ( ph /\ { c , d } e. K ) /\ ( c e. W /\ d e. W ) ) /\ ( m e. V /\ n e. V ) ) /\ ( d = ( F ` n ) /\ c = ( F ` m ) ) ) /\ e = { m , n } ) -> ( F " e ) = { ( F ` m ) , ( F ` n ) } )
68 67 eqeq2d 
 |-  ( ( ( ( ( ( ph /\ { c , d } e. K ) /\ ( c e. W /\ d e. W ) ) /\ ( m e. V /\ n e. V ) ) /\ ( d = ( F ` n ) /\ c = ( F ` m ) ) ) /\ e = { m , n } ) -> ( { c , d } = ( F " e ) <-> { c , d } = { ( F ` m ) , ( F ` n ) } ) )
69 30 adantl 
 |-  ( ( ( ( ( ph /\ { c , d } e. K ) /\ ( c e. W /\ d e. W ) ) /\ ( m e. V /\ n e. V ) ) /\ ( d = ( F ` n ) /\ c = ( F ` m ) ) ) -> { c , d } = { ( F ` m ) , ( F ` n ) } )
70 55 68 69 rspcedvd 
 |-  ( ( ( ( ( ph /\ { c , d } e. K ) /\ ( c e. W /\ d e. W ) ) /\ ( m e. V /\ n e. V ) ) /\ ( d = ( F ` n ) /\ c = ( F ` m ) ) ) -> E. e e. E { c , d } = ( F " e ) )
71 70 ex 
 |-  ( ( ( ( ph /\ { c , d } e. K ) /\ ( c e. W /\ d e. W ) ) /\ ( m e. V /\ n e. V ) ) -> ( ( d = ( F ` n ) /\ c = ( F ` m ) ) -> E. e e. E { c , d } = ( F " e ) ) )
72 71 anassrs 
 |-  ( ( ( ( ( ph /\ { c , d } e. K ) /\ ( c e. W /\ d e. W ) ) /\ m e. V ) /\ n e. V ) -> ( ( d = ( F ` n ) /\ c = ( F ` m ) ) -> E. e e. E { c , d } = ( F " e ) ) )
73 72 expd 
 |-  ( ( ( ( ( ph /\ { c , d } e. K ) /\ ( c e. W /\ d e. W ) ) /\ m e. V ) /\ n e. V ) -> ( d = ( F ` n ) -> ( c = ( F ` m ) -> E. e e. E { c , d } = ( F " e ) ) ) )
74 73 rexlimdva 
 |-  ( ( ( ( ph /\ { c , d } e. K ) /\ ( c e. W /\ d e. W ) ) /\ m e. V ) -> ( E. n e. V d = ( F ` n ) -> ( c = ( F ` m ) -> E. e e. E { c , d } = ( F " e ) ) ) )
75 74 com23 
 |-  ( ( ( ( ph /\ { c , d } e. K ) /\ ( c e. W /\ d e. W ) ) /\ m e. V ) -> ( c = ( F ` m ) -> ( E. n e. V d = ( F ` n ) -> E. e e. E { c , d } = ( F " e ) ) ) )
76 75 rexlimdva 
 |-  ( ( ( ph /\ { c , d } e. K ) /\ ( c e. W /\ d e. W ) ) -> ( E. m e. V c = ( F ` m ) -> ( E. n e. V d = ( F ` n ) -> E. e e. E { c , d } = ( F " e ) ) ) )
77 76 impd 
 |-  ( ( ( ph /\ { c , d } e. K ) /\ ( c e. W /\ d e. W ) ) -> ( ( E. m e. V c = ( F ` m ) /\ E. n e. V d = ( F ` n ) ) -> E. e e. E { c , d } = ( F " e ) ) )
78 28 77 mpd 
 |-  ( ( ( ph /\ { c , d } e. K ) /\ ( c e. W /\ d e. W ) ) -> E. e e. E { c , d } = ( F " e ) )
79 78 ex 
 |-  ( ( ph /\ { c , d } e. K ) -> ( ( c e. W /\ d e. W ) -> E. e e. E { c , d } = ( F " e ) ) )
80 17 79 syl6bi 
 |-  ( y = { c , d } -> ( ( ph /\ y e. K ) -> ( ( c e. W /\ d e. W ) -> E. e e. E { c , d } = ( F " e ) ) ) )
81 80 impd 
 |-  ( y = { c , d } -> ( ( ( ph /\ y e. K ) /\ ( c e. W /\ d e. W ) ) -> E. e e. E { c , d } = ( F " e ) ) )
82 81 impcom 
 |-  ( ( ( ( ph /\ y e. K ) /\ ( c e. W /\ d e. W ) ) /\ y = { c , d } ) -> E. e e. E { c , d } = ( F " e ) )
83 simpr 
 |-  ( ( ( ( ph /\ y e. K ) /\ ( c e. W /\ d e. W ) ) /\ y = { c , d } ) -> y = { c , d } )
84 83 adantr 
 |-  ( ( ( ( ( ph /\ y e. K ) /\ ( c e. W /\ d e. W ) ) /\ y = { c , d } ) /\ e e. E ) -> y = { c , d } )
85 9 ad4antr 
 |-  ( ( ( ( ( ph /\ y e. K ) /\ ( c e. W /\ d e. W ) ) /\ y = { c , d } ) /\ e e. E ) -> F e. X )
86 1 2 3 4 5 isomuspgrlem2a 
 |-  ( F e. X -> A. y e. E ( F " y ) = ( G ` y ) )
87 85 86 syl 
 |-  ( ( ( ( ( ph /\ y e. K ) /\ ( c e. W /\ d e. W ) ) /\ y = { c , d } ) /\ e e. E ) -> A. y e. E ( F " y ) = ( G ` y ) )
88 imaeq2 
 |-  ( y = e -> ( F " y ) = ( F " e ) )
89 fveq2 
 |-  ( y = e -> ( G ` y ) = ( G ` e ) )
90 88 89 eqeq12d 
 |-  ( y = e -> ( ( F " y ) = ( G ` y ) <-> ( F " e ) = ( G ` e ) ) )
91 90 rspcv 
 |-  ( e e. E -> ( A. y e. E ( F " y ) = ( G ` y ) -> ( F " e ) = ( G ` e ) ) )
92 eqcom 
 |-  ( ( G ` e ) = ( F " e ) <-> ( F " e ) = ( G ` e ) )
93 91 92 syl6ibr 
 |-  ( e e. E -> ( A. y e. E ( F " y ) = ( G ` y ) -> ( G ` e ) = ( F " e ) ) )
94 93 adantl 
 |-  ( ( ( ( ( ph /\ y e. K ) /\ ( c e. W /\ d e. W ) ) /\ y = { c , d } ) /\ e e. E ) -> ( A. y e. E ( F " y ) = ( G ` y ) -> ( G ` e ) = ( F " e ) ) )
95 87 94 mpd 
 |-  ( ( ( ( ( ph /\ y e. K ) /\ ( c e. W /\ d e. W ) ) /\ y = { c , d } ) /\ e e. E ) -> ( G ` e ) = ( F " e ) )
96 84 95 eqeq12d 
 |-  ( ( ( ( ( ph /\ y e. K ) /\ ( c e. W /\ d e. W ) ) /\ y = { c , d } ) /\ e e. E ) -> ( y = ( G ` e ) <-> { c , d } = ( F " e ) ) )
97 96 rexbidva 
 |-  ( ( ( ( ph /\ y e. K ) /\ ( c e. W /\ d e. W ) ) /\ y = { c , d } ) -> ( E. e e. E y = ( G ` e ) <-> E. e e. E { c , d } = ( F " e ) ) )
98 82 97 mpbird 
 |-  ( ( ( ( ph /\ y e. K ) /\ ( c e. W /\ d e. W ) ) /\ y = { c , d } ) -> E. e e. E y = ( G ` e ) )
99 98 ex 
 |-  ( ( ( ph /\ y e. K ) /\ ( c e. W /\ d e. W ) ) -> ( y = { c , d } -> E. e e. E y = ( G ` e ) ) )
100 99 rexlimdvva 
 |-  ( ( ph /\ y e. K ) -> ( E. c e. W E. d e. W y = { c , d } -> E. e e. E y = ( G ` e ) ) )
101 15 100 mpd 
 |-  ( ( ph /\ y e. K ) -> E. e e. E y = ( G ` e ) )
102 101 ralrimiva 
 |-  ( ph -> A. y e. K E. e e. E y = ( G ` e ) )
103 dffo3 
 |-  ( G : E -onto-> K <-> ( G : E --> K /\ A. y e. K E. e e. E y = ( G ` e ) ) )
104 11 102 103 sylanbrc 
 |-  ( ph -> G : E -onto-> K )