Metamath Proof Explorer

Theorem isomuspgrlem1

Description: Lemma 1 for isomuspgr . (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 )
Assertion isomuspgrlem1 
|- ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) -> ( { ( f ` a ) , ( f ` b ) } e. K -> { a , b } e. 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 simpl 
 |-  ( ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) -> g : E -1-1-onto-> K )
6 5 ad2antlr 
 |-  ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) -> g : E -1-1-onto-> K )
7 f1ocnvdm 
 |-  ( ( g : E -1-1-onto-> K /\ { ( f ` a ) , ( f ` b ) } e. K ) -> ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E )
8 6 7 sylan 
 |-  ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) -> ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E )
9 uspgrupgr 
 |-  ( A e. USPGraph -> A e. UPGraph )
10 9 adantr 
 |-  ( ( A e. USPGraph /\ B e. USPGraph ) -> A e. UPGraph )
11 10 ad4antr 
 |-  ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) -> A e. UPGraph )
12 1 3 upgredg 
 |-  ( ( A e. UPGraph /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) -> E. x e. V E. y e. V ( `' g ` { ( f ` a ) , ( f ` b ) } ) = { x , y } )
13 11 12 sylan 
 |-  ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) -> E. x e. V E. y e. V ( `' g ` { ( f ` a ) , ( f ` b ) } ) = { x , y } )
14 eleq1 
 |-  ( ( `' g ` { ( f ` a ) , ( f ` b ) } ) = { x , y } -> ( ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E <-> { x , y } e. E ) )
15 14 biimpd 
 |-  ( ( `' g ` { ( f ` a ) , ( f ` b ) } ) = { x , y } -> ( ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E -> { x , y } e. E ) )
16 15 com12 
 |-  ( ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E -> ( ( `' g ` { ( f ` a ) , ( f ` b ) } ) = { x , y } -> { x , y } e. E ) )
17 16 ad2antlr 
 |-  ( ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) /\ ( x e. V /\ y e. V ) ) -> ( ( `' g ` { ( f ` a ) , ( f ` b ) } ) = { x , y } -> { x , y } e. E ) )
18 17 imp 
 |-  ( ( ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) /\ ( x e. V /\ y e. V ) ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) = { x , y } ) -> { x , y } e. E )
19 5 ad6antlr 
 |-  ( ( ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) /\ ( x e. V /\ y e. V ) ) /\ { x , y } e. E ) -> g : E -1-1-onto-> K )
20 simpr 
 |-  ( ( ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) /\ ( x e. V /\ y e. V ) ) /\ { x , y } e. E ) -> { x , y } e. E )
21 simpr 
 |-  ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) -> { ( f ` a ) , ( f ` b ) } e. K )
22 21 ad5ant12 
 |-  ( ( ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) /\ ( x e. V /\ y e. V ) ) /\ { x , y } e. E ) -> { ( f ` a ) , ( f ` b ) } e. K )
23 19 20 22 3jca 
 |-  ( ( ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) /\ ( x e. V /\ y e. V ) ) /\ { x , y } e. E ) -> ( g : E -1-1-onto-> K /\ { x , y } e. E /\ { ( f ` a ) , ( f ` b ) } e. K ) )
24 f1ocnvfvb 
 |-  ( ( g : E -1-1-onto-> K /\ { x , y } e. E /\ { ( f ` a ) , ( f ` b ) } e. K ) -> ( ( g ` { x , y } ) = { ( f ` a ) , ( f ` b ) } <-> ( `' g ` { ( f ` a ) , ( f ` b ) } ) = { x , y } ) )
25 23 24 syl 
 |-  ( ( ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) /\ ( x e. V /\ y e. V ) ) /\ { x , y } e. E ) -> ( ( g ` { x , y } ) = { ( f ` a ) , ( f ` b ) } <-> ( `' g ` { ( f ` a ) , ( f ` b ) } ) = { x , y } ) )
26 imaeq2 
 |-  ( e = { x , y } -> ( f " e ) = ( f " { x , y } ) )
27 fveq2 
 |-  ( e = { x , y } -> ( g ` e ) = ( g ` { x , y } ) )
28 26 27 eqeq12d 
 |-  ( e = { x , y } -> ( ( f " e ) = ( g ` e ) <-> ( f " { x , y } ) = ( g ` { x , y } ) ) )
29 28 rspccv 
 |-  ( A. e e. E ( f " e ) = ( g ` e ) -> ( { x , y } e. E -> ( f " { x , y } ) = ( g ` { x , y } ) ) )
30 29 adantl 
 |-  ( ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) -> ( { x , y } e. E -> ( f " { x , y } ) = ( g ` { x , y } ) ) )
31 30 adantl 
 |-  ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) -> ( { x , y } e. E -> ( f " { x , y } ) = ( g ` { x , y } ) ) )
32 31 ad4antr 
 |-  ( ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) /\ ( x e. V /\ y e. V ) ) -> ( { x , y } e. E -> ( f " { x , y } ) = ( g ` { x , y } ) ) )
33 32 imp 
 |-  ( ( ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) /\ ( x e. V /\ y e. V ) ) /\ { x , y } e. E ) -> ( f " { x , y } ) = ( g ` { x , y } ) )
34 eqeq1 
 |-  ( ( g ` { x , y } ) = ( f " { x , y } ) -> ( ( g ` { x , y } ) = { ( f ` a ) , ( f ` b ) } <-> ( f " { x , y } ) = { ( f ` a ) , ( f ` b ) } ) )
35 34 eqcoms 
 |-  ( ( f " { x , y } ) = ( g ` { x , y } ) -> ( ( g ` { x , y } ) = { ( f ` a ) , ( f ` b ) } <-> ( f " { x , y } ) = { ( f ` a ) , ( f ` b ) } ) )
36 35 adantl 
 |-  ( ( ( ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) /\ ( x e. V /\ y e. V ) ) /\ { x , y } e. E ) /\ ( f " { x , y } ) = ( g ` { x , y } ) ) -> ( ( g ` { x , y } ) = { ( f ` a ) , ( f ` b ) } <-> ( f " { x , y } ) = { ( f ` a ) , ( f ` b ) } ) )
37 f1ofn 
 |-  ( f : V -1-1-onto-> W -> f Fn V )
38 37 ad6antlr 
 |-  ( ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) /\ ( x e. V /\ y e. V ) ) -> f Fn V )
39 simpl 
 |-  ( ( x e. V /\ y e. V ) -> x e. V )
40 39 adantl 
 |-  ( ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) /\ ( x e. V /\ y e. V ) ) -> x e. V )
41 simpr 
 |-  ( ( x e. V /\ y e. V ) -> y e. V )
42 41 adantl 
 |-  ( ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) /\ ( x e. V /\ y e. V ) ) -> y e. V )
43 38 40 42 3jca 
 |-  ( ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) /\ ( x e. V /\ y e. V ) ) -> ( f Fn V /\ x e. V /\ y e. V ) )
44 43 adantr 
 |-  ( ( ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) /\ ( x e. V /\ y e. V ) ) /\ { x , y } e. E ) -> ( f Fn V /\ x e. V /\ y e. V ) )
45 fnimapr 
 |-  ( ( f Fn V /\ x e. V /\ y e. V ) -> ( f " { x , y } ) = { ( f ` x ) , ( f ` y ) } )
46 44 45 syl 
 |-  ( ( ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) /\ ( x e. V /\ y e. V ) ) /\ { x , y } e. E ) -> ( f " { x , y } ) = { ( f ` x ) , ( f ` y ) } )
47 46 eqeq1d 
 |-  ( ( ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) /\ ( x e. V /\ y e. V ) ) /\ { x , y } e. E ) -> ( ( f " { x , y } ) = { ( f ` a ) , ( f ` b ) } <-> { ( f ` x ) , ( f ` y ) } = { ( f ` a ) , ( f ` b ) } ) )
48 fvex 
 |-  ( f ` x ) e. _V
49 fvex 
 |-  ( f ` y ) e. _V
50 fvex 
 |-  ( f ` a ) e. _V
51 fvex 
 |-  ( f ` b ) e. _V
52 48 49 50 51 preq12b 
 |-  ( { ( f ` x ) , ( f ` y ) } = { ( f ` a ) , ( f ` b ) } <-> ( ( ( f ` x ) = ( f ` a ) /\ ( f ` y ) = ( f ` b ) ) \/ ( ( f ` x ) = ( f ` b ) /\ ( f ` y ) = ( f ` a ) ) ) )
53 f1of1 
 |-  ( f : V -1-1-onto-> W -> f : V -1-1-> W )
54 simpl 
 |-  ( ( a e. V /\ b e. V ) -> a e. V )
55 54 39 anim12ci 
 |-  ( ( ( a e. V /\ b e. V ) /\ ( x e. V /\ y e. V ) ) -> ( x e. V /\ a e. V ) )
56 f1veqaeq 
 |-  ( ( f : V -1-1-> W /\ ( x e. V /\ a e. V ) ) -> ( ( f ` x ) = ( f ` a ) -> x = a ) )
57 53 55 56 syl2anr 
 |-  ( ( ( ( a e. V /\ b e. V ) /\ ( x e. V /\ y e. V ) ) /\ f : V -1-1-onto-> W ) -> ( ( f ` x ) = ( f ` a ) -> x = a ) )
58 simpr 
 |-  ( ( a e. V /\ b e. V ) -> b e. V )
59 58 41 anim12ci 
 |-  ( ( ( a e. V /\ b e. V ) /\ ( x e. V /\ y e. V ) ) -> ( y e. V /\ b e. V ) )
60 f1veqaeq 
 |-  ( ( f : V -1-1-> W /\ ( y e. V /\ b e. V ) ) -> ( ( f ` y ) = ( f ` b ) -> y = b ) )
61 53 59 60 syl2anr 
 |-  ( ( ( ( a e. V /\ b e. V ) /\ ( x e. V /\ y e. V ) ) /\ f : V -1-1-onto-> W ) -> ( ( f ` y ) = ( f ` b ) -> y = b ) )
62 57 61 anim12d 
 |-  ( ( ( ( a e. V /\ b e. V ) /\ ( x e. V /\ y e. V ) ) /\ f : V -1-1-onto-> W ) -> ( ( ( f ` x ) = ( f ` a ) /\ ( f ` y ) = ( f ` b ) ) -> ( x = a /\ y = b ) ) )
63 62 impcom 
 |-  ( ( ( ( f ` x ) = ( f ` a ) /\ ( f ` y ) = ( f ` b ) ) /\ ( ( ( a e. V /\ b e. V ) /\ ( x e. V /\ y e. V ) ) /\ f : V -1-1-onto-> W ) ) -> ( x = a /\ y = b ) )
64 63 orcd 
 |-  ( ( ( ( f ` x ) = ( f ` a ) /\ ( f ` y ) = ( f ` b ) ) /\ ( ( ( a e. V /\ b e. V ) /\ ( x e. V /\ y e. V ) ) /\ f : V -1-1-onto-> W ) ) -> ( ( x = a /\ y = b ) \/ ( x = b /\ y = a ) ) )
65 64 ex 
 |-  ( ( ( f ` x ) = ( f ` a ) /\ ( f ` y ) = ( f ` b ) ) -> ( ( ( ( a e. V /\ b e. V ) /\ ( x e. V /\ y e. V ) ) /\ f : V -1-1-onto-> W ) -> ( ( x = a /\ y = b ) \/ ( x = b /\ y = a ) ) ) )
66 58 39 anim12ci 
 |-  ( ( ( a e. V /\ b e. V ) /\ ( x e. V /\ y e. V ) ) -> ( x e. V /\ b e. V ) )
67 f1veqaeq 
 |-  ( ( f : V -1-1-> W /\ ( x e. V /\ b e. V ) ) -> ( ( f ` x ) = ( f ` b ) -> x = b ) )
68 53 66 67 syl2anr 
 |-  ( ( ( ( a e. V /\ b e. V ) /\ ( x e. V /\ y e. V ) ) /\ f : V -1-1-onto-> W ) -> ( ( f ` x ) = ( f ` b ) -> x = b ) )
69 54 41 anim12ci 
 |-  ( ( ( a e. V /\ b e. V ) /\ ( x e. V /\ y e. V ) ) -> ( y e. V /\ a e. V ) )
70 f1veqaeq 
 |-  ( ( f : V -1-1-> W /\ ( y e. V /\ a e. V ) ) -> ( ( f ` y ) = ( f ` a ) -> y = a ) )
71 53 69 70 syl2anr 
 |-  ( ( ( ( a e. V /\ b e. V ) /\ ( x e. V /\ y e. V ) ) /\ f : V -1-1-onto-> W ) -> ( ( f ` y ) = ( f ` a ) -> y = a ) )
72 68 71 anim12d 
 |-  ( ( ( ( a e. V /\ b e. V ) /\ ( x e. V /\ y e. V ) ) /\ f : V -1-1-onto-> W ) -> ( ( ( f ` x ) = ( f ` b ) /\ ( f ` y ) = ( f ` a ) ) -> ( x = b /\ y = a ) ) )
73 72 impcom 
 |-  ( ( ( ( f ` x ) = ( f ` b ) /\ ( f ` y ) = ( f ` a ) ) /\ ( ( ( a e. V /\ b e. V ) /\ ( x e. V /\ y e. V ) ) /\ f : V -1-1-onto-> W ) ) -> ( x = b /\ y = a ) )
74 73 olcd 
 |-  ( ( ( ( f ` x ) = ( f ` b ) /\ ( f ` y ) = ( f ` a ) ) /\ ( ( ( a e. V /\ b e. V ) /\ ( x e. V /\ y e. V ) ) /\ f : V -1-1-onto-> W ) ) -> ( ( x = a /\ y = b ) \/ ( x = b /\ y = a ) ) )
75 74 ex 
 |-  ( ( ( f ` x ) = ( f ` b ) /\ ( f ` y ) = ( f ` a ) ) -> ( ( ( ( a e. V /\ b e. V ) /\ ( x e. V /\ y e. V ) ) /\ f : V -1-1-onto-> W ) -> ( ( x = a /\ y = b ) \/ ( x = b /\ y = a ) ) ) )
76 65 75 jaoi 
 |-  ( ( ( ( f ` x ) = ( f ` a ) /\ ( f ` y ) = ( f ` b ) ) \/ ( ( f ` x ) = ( f ` b ) /\ ( f ` y ) = ( f ` a ) ) ) -> ( ( ( ( a e. V /\ b e. V ) /\ ( x e. V /\ y e. V ) ) /\ f : V -1-1-onto-> W ) -> ( ( x = a /\ y = b ) \/ ( x = b /\ y = a ) ) ) )
77 vex 
 |-  x e. _V
78 vex 
 |-  y e. _V
79 vex 
 |-  a e. _V
80 vex 
 |-  b e. _V
81 77 78 79 80 preq12b 
 |-  ( { x , y } = { a , b } <-> ( ( x = a /\ y = b ) \/ ( x = b /\ y = a ) ) )
82 76 81 syl6ibr 
 |-  ( ( ( ( f ` x ) = ( f ` a ) /\ ( f ` y ) = ( f ` b ) ) \/ ( ( f ` x ) = ( f ` b ) /\ ( f ` y ) = ( f ` a ) ) ) -> ( ( ( ( a e. V /\ b e. V ) /\ ( x e. V /\ y e. V ) ) /\ f : V -1-1-onto-> W ) -> { x , y } = { a , b } ) )
83 52 82 sylbi 
 |-  ( { ( f ` x ) , ( f ` y ) } = { ( f ` a ) , ( f ` b ) } -> ( ( ( ( a e. V /\ b e. V ) /\ ( x e. V /\ y e. V ) ) /\ f : V -1-1-onto-> W ) -> { x , y } = { a , b } ) )
84 83 com12 
 |-  ( ( ( ( a e. V /\ b e. V ) /\ ( x e. V /\ y e. V ) ) /\ f : V -1-1-onto-> W ) -> ( { ( f ` x ) , ( f ` y ) } = { ( f ` a ) , ( f ` b ) } -> { x , y } = { a , b } ) )
85 84 expcom 
 |-  ( f : V -1-1-onto-> W -> ( ( ( a e. V /\ b e. V ) /\ ( x e. V /\ y e. V ) ) -> ( { ( f ` x ) , ( f ` y ) } = { ( f ` a ) , ( f ` b ) } -> { x , y } = { a , b } ) ) )
86 85 expd 
 |-  ( f : V -1-1-onto-> W -> ( ( a e. V /\ b e. V ) -> ( ( x e. V /\ y e. V ) -> ( { ( f ` x ) , ( f ` y ) } = { ( f ` a ) , ( f ` b ) } -> { x , y } = { a , b } ) ) ) )
87 86 ad2antlr 
 |-  ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) -> ( ( a e. V /\ b e. V ) -> ( ( x e. V /\ y e. V ) -> ( { ( f ` x ) , ( f ` y ) } = { ( f ` a ) , ( f ` b ) } -> { x , y } = { a , b } ) ) ) )
88 87 imp 
 |-  ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) -> ( ( x e. V /\ y e. V ) -> ( { ( f ` x ) , ( f ` y ) } = { ( f ` a ) , ( f ` b ) } -> { x , y } = { a , b } ) ) )
89 88 adantr 
 |-  ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) -> ( ( x e. V /\ y e. V ) -> ( { ( f ` x ) , ( f ` y ) } = { ( f ` a ) , ( f ` b ) } -> { x , y } = { a , b } ) ) )
90 89 adantr 
 |-  ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) -> ( ( x e. V /\ y e. V ) -> ( { ( f ` x ) , ( f ` y ) } = { ( f ` a ) , ( f ` b ) } -> { x , y } = { a , b } ) ) )
91 90 imp31 
 |-  ( ( ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) /\ ( x e. V /\ y e. V ) ) /\ { ( f ` x ) , ( f ` y ) } = { ( f ` a ) , ( f ` b ) } ) -> { x , y } = { a , b } )
92 91 eleq1d 
 |-  ( ( ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) /\ ( x e. V /\ y e. V ) ) /\ { ( f ` x ) , ( f ` y ) } = { ( f ` a ) , ( f ` b ) } ) -> ( { x , y } e. E <-> { a , b } e. E ) )
93 92 biimpd 
 |-  ( ( ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) /\ ( x e. V /\ y e. V ) ) /\ { ( f ` x ) , ( f ` y ) } = { ( f ` a ) , ( f ` b ) } ) -> ( { x , y } e. E -> { a , b } e. E ) )
94 93 impancom 
 |-  ( ( ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) /\ ( x e. V /\ y e. V ) ) /\ { x , y } e. E ) -> ( { ( f ` x ) , ( f ` y ) } = { ( f ` a ) , ( f ` b ) } -> { a , b } e. E ) )
95 47 94 sylbid 
 |-  ( ( ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) /\ ( x e. V /\ y e. V ) ) /\ { x , y } e. E ) -> ( ( f " { x , y } ) = { ( f ` a ) , ( f ` b ) } -> { a , b } e. E ) )
96 95 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) /\ ( x e. V /\ y e. V ) ) /\ { x , y } e. E ) /\ ( f " { x , y } ) = ( g ` { x , y } ) ) -> ( ( f " { x , y } ) = { ( f ` a ) , ( f ` b ) } -> { a , b } e. E ) )
97 36 96 sylbid 
 |-  ( ( ( ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) /\ ( x e. V /\ y e. V ) ) /\ { x , y } e. E ) /\ ( f " { x , y } ) = ( g ` { x , y } ) ) -> ( ( g ` { x , y } ) = { ( f ` a ) , ( f ` b ) } -> { a , b } e. E ) )
98 33 97 mpdan 
 |-  ( ( ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) /\ ( x e. V /\ y e. V ) ) /\ { x , y } e. E ) -> ( ( g ` { x , y } ) = { ( f ` a ) , ( f ` b ) } -> { a , b } e. E ) )
99 25 98 sylbird 
 |-  ( ( ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) /\ ( x e. V /\ y e. V ) ) /\ { x , y } e. E ) -> ( ( `' g ` { ( f ` a ) , ( f ` b ) } ) = { x , y } -> { a , b } e. E ) )
100 99 impancom 
 |-  ( ( ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) /\ ( x e. V /\ y e. V ) ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) = { x , y } ) -> ( { x , y } e. E -> { a , b } e. E ) )
101 18 100 mpd 
 |-  ( ( ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) /\ ( x e. V /\ y e. V ) ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) = { x , y } ) -> { a , b } e. E )
102 101 ex 
 |-  ( ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) /\ ( x e. V /\ y e. V ) ) -> ( ( `' g ` { ( f ` a ) , ( f ` b ) } ) = { x , y } -> { a , b } e. E ) )
103 102 rexlimdvva 
 |-  ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) -> ( E. x e. V E. y e. V ( `' g ` { ( f ` a ) , ( f ` b ) } ) = { x , y } -> { a , b } e. E ) )
104 13 103 mpd 
 |-  ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) /\ ( `' g ` { ( f ` a ) , ( f ` b ) } ) e. E ) -> { a , b } e. E )
105 8 104 mpdan 
 |-  ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) /\ { ( f ` a ) , ( f ` b ) } e. K ) -> { a , b } e. E )
106 105 ex 
 |-  ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) -> ( { ( f ` a ) , ( f ` b ) } e. K -> { a , b } e. E ) )