Metamath Proof Explorer

Theorem isomuspgrlem2

Description: Lemma 2 for isomuspgr . (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 )
Assertion isomuspgrlem2 
|- ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) -> ( A. a e. V A. b e. V ( { a , b } e. E <-> { ( f ` a ) , ( f ` b ) } e. K ) -> E. g ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) )

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 3 fvexi 
 |-  E e. _V
6 5 mptex 
 |-  ( x e. E |-> ( f " x ) ) e. _V
7 eqid 
 |-  ( x e. E |-> ( f " x ) ) = ( x e. E |-> ( f " x ) )
8 simplll 
 |-  ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ A. a e. V A. b e. V ( { a , b } e. E <-> { ( f ` a ) , ( f ` b ) } e. K ) ) -> A e. USPGraph )
9 simplr 
 |-  ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ A. a e. V A. b e. V ( { a , b } e. E <-> { ( f ` a ) , ( f ` b ) } e. K ) ) -> f : V -1-1-onto-> W )
10 simpr 
 |-  ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ A. a e. V A. b e. V ( { a , b } e. E <-> { ( f ` a ) , ( f ` b ) } e. K ) ) -> A. a e. V A. b e. V ( { a , b } e. E <-> { ( f ` a ) , ( f ` b ) } e. K ) )
11 vex 
 |-  f e. _V
12 11 a1i 
 |-  ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ A. a e. V A. b e. V ( { a , b } e. E <-> { ( f ` a ) , ( f ` b ) } e. K ) ) -> f e. _V )
13 simpllr 
 |-  ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ A. a e. V A. b e. V ( { a , b } e. E <-> { ( f ` a ) , ( f ` b ) } e. K ) ) -> B e. USPGraph )
14 1 2 3 4 7 8 9 10 12 13 isomuspgrlem2e 
 |-  ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ A. a e. V A. b e. V ( { a , b } e. E <-> { ( f ` a ) , ( f ` b ) } e. K ) ) -> ( x e. E |-> ( f " x ) ) : E -1-1-onto-> K )
15 1 2 3 4 7 isomuspgrlem2a 
 |-  ( f e. _V -> A. e e. E ( f " e ) = ( ( x e. E |-> ( f " x ) ) ` e ) )
16 11 15 mp1i 
 |-  ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ A. a e. V A. b e. V ( { a , b } e. E <-> { ( f ` a ) , ( f ` b ) } e. K ) ) -> A. e e. E ( f " e ) = ( ( x e. E |-> ( f " x ) ) ` e ) )
17 14 16 jca 
 |-  ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ A. a e. V A. b e. V ( { a , b } e. E <-> { ( f ` a ) , ( f ` b ) } e. K ) ) -> ( ( x e. E |-> ( f " x ) ) : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( ( x e. E |-> ( f " x ) ) ` e ) ) )
18 f1oeq1 
 |-  ( g = ( x e. E |-> ( f " x ) ) -> ( g : E -1-1-onto-> K <-> ( x e. E |-> ( f " x ) ) : E -1-1-onto-> K ) )
19 fveq1 
 |-  ( g = ( x e. E |-> ( f " x ) ) -> ( g ` e ) = ( ( x e. E |-> ( f " x ) ) ` e ) )
20 19 eqeq2d 
 |-  ( g = ( x e. E |-> ( f " x ) ) -> ( ( f " e ) = ( g ` e ) <-> ( f " e ) = ( ( x e. E |-> ( f " x ) ) ` e ) ) )
21 20 ralbidv 
 |-  ( g = ( x e. E |-> ( f " x ) ) -> ( A. e e. E ( f " e ) = ( g ` e ) <-> A. e e. E ( f " e ) = ( ( x e. E |-> ( f " x ) ) ` e ) ) )
22 18 21 anbi12d 
 |-  ( g = ( x e. E |-> ( f " x ) ) -> ( ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) <-> ( ( x e. E |-> ( f " x ) ) : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( ( x e. E |-> ( f " x ) ) ` e ) ) ) )
23 22 spcegv 
 |-  ( ( x e. E |-> ( f " x ) ) e. _V -> ( ( ( x e. E |-> ( f " x ) ) : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( ( x e. E |-> ( f " x ) ) ` e ) ) -> E. g ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) )
24 6 17 23 mpsyl 
 |-  ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ A. a e. V A. b e. V ( { a , b } e. E <-> { ( f ` a ) , ( f ` b ) } e. K ) ) -> E. g ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) )
25 24 ex 
 |-  ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) -> ( A. a e. V A. b e. V ( { a , b } e. E <-> { ( f ` a ) , ( f ` b ) } e. K ) -> E. g ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) )