Metamath Proof Explorer

Theorem isuspgrimlem

Description: Lemma for isuspgrim . (Contributed by AV, 27-Apr-2025)

Ref Expression
Hypotheses isusgrim.v 
|- V = ( Vtx ` G )
isusgrim.w 
|- W = ( Vtx ` H )
isusgrim.e 
|- E = ( Edg ` G )
isusgrim.d 
|- D = ( Edg ` H )
Assertion isuspgrimlem 
|- ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) -> ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D )

Proof

Step Hyp Ref Expression
1 isusgrim.v 
 |-  V = ( Vtx ` G )
2 isusgrim.w 
 |-  W = ( Vtx ` H )
3 isusgrim.e 
 |-  E = ( Edg ` G )
4 isusgrim.d 
 |-  D = ( Edg ` H )
5 uspgrupgr 
 |-  ( G e. USPGraph -> G e. UPGraph )
6 5 adantr 
 |-  ( ( G e. USPGraph /\ H e. USPGraph ) -> G e. UPGraph )
7 6 adantr 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) -> G e. UPGraph )
8 7 adantr 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) -> G e. UPGraph )
9 1 3 upgredg 
 |-  ( ( G e. UPGraph /\ e e. E ) -> E. a e. V E. b e. V e = { a , b } )
10 8 9 sylan 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ e e. E ) -> E. a e. V E. b e. V e = { a , b } )
11 preq12 
 |-  ( ( x = a /\ y = b ) -> { x , y } = { a , b } )
12 11 eleq1d 
 |-  ( ( x = a /\ y = b ) -> ( { x , y } e. E <-> { a , b } e. E ) )
13 fveq2 
 |-  ( x = a -> ( F ` x ) = ( F ` a ) )
14 13 adantr 
 |-  ( ( x = a /\ y = b ) -> ( F ` x ) = ( F ` a ) )
15 fveq2 
 |-  ( y = b -> ( F ` y ) = ( F ` b ) )
16 15 adantl 
 |-  ( ( x = a /\ y = b ) -> ( F ` y ) = ( F ` b ) )
17 14 16 preq12d 
 |-  ( ( x = a /\ y = b ) -> { ( F ` x ) , ( F ` y ) } = { ( F ` a ) , ( F ` b ) } )
18 17 eleq1d 
 |-  ( ( x = a /\ y = b ) -> ( { ( F ` x ) , ( F ` y ) } e. D <-> { ( F ` a ) , ( F ` b ) } e. D ) )
19 12 18 bibi12d 
 |-  ( ( x = a /\ y = b ) -> ( ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) <-> ( { a , b } e. E <-> { ( F ` a ) , ( F ` b ) } e. D ) ) )
20 19 rspc2gv 
 |-  ( ( a e. V /\ b e. V ) -> ( A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) -> ( { a , b } e. E <-> { ( F ` a ) , ( F ` b ) } e. D ) ) )
21 20 com12 
 |-  ( A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) -> ( ( a e. V /\ b e. V ) -> ( { a , b } e. E <-> { ( F ` a ) , ( F ` b ) } e. D ) ) )
22 21 adantl 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) -> ( ( a e. V /\ b e. V ) -> ( { a , b } e. E <-> { ( F ` a ) , ( F ` b ) } e. D ) ) )
23 22 imp 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ ( a e. V /\ b e. V ) ) -> ( { a , b } e. E <-> { ( F ` a ) , ( F ` b ) } e. D ) )
24 f1ofn 
 |-  ( F : V -1-1-onto-> W -> F Fn V )
25 24 ad3antlr 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ ( a e. V /\ b e. V ) ) -> F Fn V )
26 simprl 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ ( a e. V /\ b e. V ) ) -> a e. V )
27 simpr 
 |-  ( ( a e. V /\ b e. V ) -> b e. V )
28 27 adantl 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ ( a e. V /\ b e. V ) ) -> b e. V )
29 fnimapr 
 |-  ( ( F Fn V /\ a e. V /\ b e. V ) -> ( F " { a , b } ) = { ( F ` a ) , ( F ` b ) } )
30 25 26 28 29 syl3anc 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ ( a e. V /\ b e. V ) ) -> ( F " { a , b } ) = { ( F ` a ) , ( F ` b ) } )
31 30 eqcomd 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ ( a e. V /\ b e. V ) ) -> { ( F ` a ) , ( F ` b ) } = ( F " { a , b } ) )
32 31 eleq1d 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ ( a e. V /\ b e. V ) ) -> ( { ( F ` a ) , ( F ` b ) } e. D <-> ( F " { a , b } ) e. D ) )
33 23 32 bitrd 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ ( a e. V /\ b e. V ) ) -> ( { a , b } e. E <-> ( F " { a , b } ) e. D ) )
34 33 adantr 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ ( a e. V /\ b e. V ) ) /\ e = { a , b } ) -> ( { a , b } e. E <-> ( F " { a , b } ) e. D ) )
35 34 biimpd 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ ( a e. V /\ b e. V ) ) /\ e = { a , b } ) -> ( { a , b } e. E -> ( F " { a , b } ) e. D ) )
36 eleq1 
 |-  ( e = { a , b } -> ( e e. E <-> { a , b } e. E ) )
37 imaeq2 
 |-  ( e = { a , b } -> ( F " e ) = ( F " { a , b } ) )
38 37 eleq1d 
 |-  ( e = { a , b } -> ( ( F " e ) e. D <-> ( F " { a , b } ) e. D ) )
39 36 38 imbi12d 
 |-  ( e = { a , b } -> ( ( e e. E -> ( F " e ) e. D ) <-> ( { a , b } e. E -> ( F " { a , b } ) e. D ) ) )
40 39 adantl 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ ( a e. V /\ b e. V ) ) /\ e = { a , b } ) -> ( ( e e. E -> ( F " e ) e. D ) <-> ( { a , b } e. E -> ( F " { a , b } ) e. D ) ) )
41 35 40 mpbird 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ ( a e. V /\ b e. V ) ) /\ e = { a , b } ) -> ( e e. E -> ( F " e ) e. D ) )
42 41 exp31 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) -> ( ( a e. V /\ b e. V ) -> ( e = { a , b } -> ( e e. E -> ( F " e ) e. D ) ) ) )
43 42 com23 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) -> ( e = { a , b } -> ( ( a e. V /\ b e. V ) -> ( e e. E -> ( F " e ) e. D ) ) ) )
44 43 com24 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) -> ( e e. E -> ( ( a e. V /\ b e. V ) -> ( e = { a , b } -> ( F " e ) e. D ) ) ) )
45 44 imp 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ e e. E ) -> ( ( a e. V /\ b e. V ) -> ( e = { a , b } -> ( F " e ) e. D ) ) )
46 45 rexlimdvv 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ e e. E ) -> ( E. a e. V E. b e. V e = { a , b } -> ( F " e ) e. D ) )
47 10 46 mpd 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ e e. E ) -> ( F " e ) e. D )
48 47 ex 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) -> ( e e. E -> ( F " e ) e. D ) )
49 48 ralrimiv 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) -> A. e e. E ( F " e ) e. D )
50 uspgrupgr 
 |-  ( H e. USPGraph -> H e. UPGraph )
51 50 ad3antlr 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) -> H e. UPGraph )
52 2 4 upgredg 
 |-  ( ( H e. UPGraph /\ d e. D ) -> E. a e. W E. b e. W d = { a , b } )
53 51 52 sylan 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ d e. D ) -> E. a e. W E. b e. W d = { a , b } )
54 f1ofo 
 |-  ( F : V -1-1-onto-> W -> F : V -onto-> W )
55 foelrn 
 |-  ( ( F : V -onto-> W /\ a e. W ) -> E. m e. V a = ( F ` m ) )
56 55 ex 
 |-  ( F : V -onto-> W -> ( a e. W -> E. m e. V a = ( F ` m ) ) )
57 foelrn 
 |-  ( ( F : V -onto-> W /\ b e. W ) -> E. n e. V b = ( F ` n ) )
58 57 ex 
 |-  ( F : V -onto-> W -> ( b e. W -> E. n e. V b = ( F ` n ) ) )
59 56 58 anim12d 
 |-  ( F : V -onto-> W -> ( ( a e. W /\ b e. W ) -> ( E. m e. V a = ( F ` m ) /\ E. n e. V b = ( F ` n ) ) ) )
60 54 59 syl 
 |-  ( F : V -1-1-onto-> W -> ( ( a e. W /\ b e. W ) -> ( E. m e. V a = ( F ` m ) /\ E. n e. V b = ( F ` n ) ) ) )
61 60 adantl 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) -> ( ( a e. W /\ b e. W ) -> ( E. m e. V a = ( F ` m ) /\ E. n e. V b = ( F ` n ) ) ) )
62 61 adantr 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) -> ( ( a e. W /\ b e. W ) -> ( E. m e. V a = ( F ` m ) /\ E. n e. V b = ( F ` n ) ) ) )
63 62 imp 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ ( a e. W /\ b e. W ) ) -> ( E. m e. V a = ( F ` m ) /\ E. n e. V b = ( F ` n ) ) )
64 preq12 
 |-  ( ( a = ( F ` m ) /\ b = ( F ` n ) ) -> { a , b } = { ( F ` m ) , ( F ` n ) } )
65 64 eqeq2d 
 |-  ( ( a = ( F ` m ) /\ b = ( F ` n ) ) -> ( d = { a , b } <-> d = { ( F ` m ) , ( F ` n ) } ) )
66 65 ancoms 
 |-  ( ( b = ( F ` n ) /\ a = ( F ` m ) ) -> ( d = { a , b } <-> d = { ( F ` m ) , ( F ` n ) } ) )
67 66 adantl 
 |-  ( ( ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ ( a e. W /\ b e. W ) ) /\ m e. V ) /\ n e. V ) /\ ( b = ( F ` n ) /\ a = ( F ` m ) ) ) -> ( d = { a , b } <-> d = { ( F ` m ) , ( F ` n ) } ) )
68 preq12 
 |-  ( ( x = m /\ y = n ) -> { x , y } = { m , n } )
69 68 eleq1d 
 |-  ( ( x = m /\ y = n ) -> ( { x , y } e. E <-> { m , n } e. E ) )
70 fveq2 
 |-  ( x = m -> ( F ` x ) = ( F ` m ) )
71 70 adantr 
 |-  ( ( x = m /\ y = n ) -> ( F ` x ) = ( F ` m ) )
72 fveq2 
 |-  ( y = n -> ( F ` y ) = ( F ` n ) )
73 72 adantl 
 |-  ( ( x = m /\ y = n ) -> ( F ` y ) = ( F ` n ) )
74 71 73 preq12d 
 |-  ( ( x = m /\ y = n ) -> { ( F ` x ) , ( F ` y ) } = { ( F ` m ) , ( F ` n ) } )
75 74 eleq1d 
 |-  ( ( x = m /\ y = n ) -> ( { ( F ` x ) , ( F ` y ) } e. D <-> { ( F ` m ) , ( F ` n ) } e. D ) )
76 69 75 bibi12d 
 |-  ( ( x = m /\ y = n ) -> ( ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) <-> ( { m , n } e. E <-> { ( F ` m ) , ( F ` n ) } e. D ) ) )
77 76 rspc2gv 
 |-  ( ( m e. V /\ n e. V ) -> ( A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) -> ( { m , n } e. E <-> { ( F ` m ) , ( F ` n ) } e. D ) ) )
78 77 adantl 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( m e. V /\ n e. V ) ) -> ( A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) -> ( { m , n } e. E <-> { ( F ` m ) , ( F ` n ) } e. D ) ) )
79 24 adantl 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) -> F Fn V )
80 79 anim1i 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( m e. V /\ n e. V ) ) -> ( F Fn V /\ ( m e. V /\ n e. V ) ) )
81 3anass 
 |-  ( ( F Fn V /\ m e. V /\ n e. V ) <-> ( F Fn V /\ ( m e. V /\ n e. V ) ) )
82 80 81 sylibr 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( m e. V /\ n e. V ) ) -> ( F Fn V /\ m e. V /\ n e. V ) )
83 fnimapr 
 |-  ( ( F Fn V /\ m e. V /\ n e. V ) -> ( F " { m , n } ) = { ( F ` m ) , ( F ` n ) } )
84 82 83 syl 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( m e. V /\ n e. V ) ) -> ( F " { m , n } ) = { ( F ` m ) , ( F ` n ) } )
85 84 eqcomd 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( m e. V /\ n e. V ) ) -> { ( F ` m ) , ( F ` n ) } = ( F " { m , n } ) )
86 simpr 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( m e. V /\ n e. V ) ) /\ ( { m , n } e. E <-> ( F " { m , n } ) e. D ) ) -> ( { m , n } e. E <-> ( F " { m , n } ) e. D ) )
87 simpr 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( m e. V /\ n e. V ) ) /\ { m , n } e. E ) -> { m , n } e. E )
88 reueq 
 |-  ( { m , n } e. E <-> E! e e. E e = { m , n } )
89 87 88 sylib 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( m e. V /\ n e. V ) ) /\ { m , n } e. E ) -> E! e e. E e = { m , n } )
90 eqcom 
 |-  ( { m , n } = e <-> e = { m , n } )
91 90 reubii 
 |-  ( E! e e. E { m , n } = e <-> E! e e. E e = { m , n } )
92 89 91 sylibr 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( m e. V /\ n e. V ) ) /\ { m , n } e. E ) -> E! e e. E { m , n } = e )
93 f1of1 
 |-  ( F : V -1-1-onto-> W -> F : V -1-1-> W )
94 93 adantl 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) -> F : V -1-1-> W )
95 94 ad5ant12 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( m e. V /\ n e. V ) ) /\ { m , n } e. E ) /\ e e. E ) -> F : V -1-1-> W )
96 prssi 
 |-  ( ( m e. V /\ n e. V ) -> { m , n } C_ V )
97 96 ad3antlr 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( m e. V /\ n e. V ) ) /\ { m , n } e. E ) /\ e e. E ) -> { m , n } C_ V )
98 uspgruhgr 
 |-  ( G e. USPGraph -> G e. UHGraph )
99 98 adantr 
 |-  ( ( G e. USPGraph /\ H e. USPGraph ) -> G e. UHGraph )
100 99 ad5ant12 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( m e. V /\ n e. V ) ) /\ { m , n } e. E ) -> G e. UHGraph )
101 3 eleq2i 
 |-  ( e e. E <-> e e. ( Edg ` G ) )
102 101 biimpi 
 |-  ( e e. E -> e e. ( Edg ` G ) )
103 edguhgr 
 |-  ( ( G e. UHGraph /\ e e. ( Edg ` G ) ) -> e e. ~P ( Vtx ` G ) )
104 1 pweqi 
 |-  ~P V = ~P ( Vtx ` G )
105 103 104 eleqtrrdi 
 |-  ( ( G e. UHGraph /\ e e. ( Edg ` G ) ) -> e e. ~P V )
106 100 102 105 syl2an 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( m e. V /\ n e. V ) ) /\ { m , n } e. E ) /\ e e. E ) -> e e. ~P V )
107 106 elpwid 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( m e. V /\ n e. V ) ) /\ { m , n } e. E ) /\ e e. E ) -> e C_ V )
108 f1imaeq 
 |-  ( ( F : V -1-1-> W /\ ( { m , n } C_ V /\ e C_ V ) ) -> ( ( F " { m , n } ) = ( F " e ) <-> { m , n } = e ) )
109 95 97 107 108 syl12anc 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( m e. V /\ n e. V ) ) /\ { m , n } e. E ) /\ e e. E ) -> ( ( F " { m , n } ) = ( F " e ) <-> { m , n } = e ) )
110 109 reubidva 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( m e. V /\ n e. V ) ) /\ { m , n } e. E ) -> ( E! e e. E ( F " { m , n } ) = ( F " e ) <-> E! e e. E { m , n } = e ) )
111 92 110 mpbird 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( m e. V /\ n e. V ) ) /\ { m , n } e. E ) -> E! e e. E ( F " { m , n } ) = ( F " e ) )
112 111 ex 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( m e. V /\ n e. V ) ) -> ( { m , n } e. E -> E! e e. E ( F " { m , n } ) = ( F " e ) ) )
113 112 adantr 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( m e. V /\ n e. V ) ) /\ ( { m , n } e. E <-> ( F " { m , n } ) e. D ) ) -> ( { m , n } e. E -> E! e e. E ( F " { m , n } ) = ( F " e ) ) )
114 86 113 sylbird 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( m e. V /\ n e. V ) ) /\ ( { m , n } e. E <-> ( F " { m , n } ) e. D ) ) -> ( ( F " { m , n } ) e. D -> E! e e. E ( F " { m , n } ) = ( F " e ) ) )
115 114 ex 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( m e. V /\ n e. V ) ) -> ( ( { m , n } e. E <-> ( F " { m , n } ) e. D ) -> ( ( F " { m , n } ) e. D -> E! e e. E ( F " { m , n } ) = ( F " e ) ) ) )
116 eleq1 
 |-  ( { ( F ` m ) , ( F ` n ) } = ( F " { m , n } ) -> ( { ( F ` m ) , ( F ` n ) } e. D <-> ( F " { m , n } ) e. D ) )
117 116 bibi2d 
 |-  ( { ( F ` m ) , ( F ` n ) } = ( F " { m , n } ) -> ( ( { m , n } e. E <-> { ( F ` m ) , ( F ` n ) } e. D ) <-> ( { m , n } e. E <-> ( F " { m , n } ) e. D ) ) )
118 eqeq1 
 |-  ( { ( F ` m ) , ( F ` n ) } = ( F " { m , n } ) -> ( { ( F ` m ) , ( F ` n ) } = ( F " e ) <-> ( F " { m , n } ) = ( F " e ) ) )
119 118 reubidv 
 |-  ( { ( F ` m ) , ( F ` n ) } = ( F " { m , n } ) -> ( E! e e. E { ( F ` m ) , ( F ` n ) } = ( F " e ) <-> E! e e. E ( F " { m , n } ) = ( F " e ) ) )
120 116 119 imbi12d 
 |-  ( { ( F ` m ) , ( F ` n ) } = ( F " { m , n } ) -> ( ( { ( F ` m ) , ( F ` n ) } e. D -> E! e e. E { ( F ` m ) , ( F ` n ) } = ( F " e ) ) <-> ( ( F " { m , n } ) e. D -> E! e e. E ( F " { m , n } ) = ( F " e ) ) ) )
121 117 120 imbi12d 
 |-  ( { ( F ` m ) , ( F ` n ) } = ( F " { m , n } ) -> ( ( ( { m , n } e. E <-> { ( F ` m ) , ( F ` n ) } e. D ) -> ( { ( F ` m ) , ( F ` n ) } e. D -> E! e e. E { ( F ` m ) , ( F ` n ) } = ( F " e ) ) ) <-> ( ( { m , n } e. E <-> ( F " { m , n } ) e. D ) -> ( ( F " { m , n } ) e. D -> E! e e. E ( F " { m , n } ) = ( F " e ) ) ) ) )
122 115 121 syl5ibrcom 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( m e. V /\ n e. V ) ) -> ( { ( F ` m ) , ( F ` n ) } = ( F " { m , n } ) -> ( ( { m , n } e. E <-> { ( F ` m ) , ( F ` n ) } e. D ) -> ( { ( F ` m ) , ( F ` n ) } e. D -> E! e e. E { ( F ` m ) , ( F ` n ) } = ( F " e ) ) ) ) )
123 85 122 mpd 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( m e. V /\ n e. V ) ) -> ( ( { m , n } e. E <-> { ( F ` m ) , ( F ` n ) } e. D ) -> ( { ( F ` m ) , ( F ` n ) } e. D -> E! e e. E { ( F ` m ) , ( F ` n ) } = ( F " e ) ) ) )
124 78 123 syld 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( m e. V /\ n e. V ) ) -> ( A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) -> ( { ( F ` m ) , ( F ` n ) } e. D -> E! e e. E { ( F ` m ) , ( F ` n ) } = ( F " e ) ) ) )
125 124 impancom 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) -> ( ( m e. V /\ n e. V ) -> ( { ( F ` m ) , ( F ` n ) } e. D -> E! e e. E { ( F ` m ) , ( F ` n ) } = ( F " e ) ) ) )
126 125 adantr 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ ( a e. W /\ b e. W ) ) -> ( ( m e. V /\ n e. V ) -> ( { ( F ` m ) , ( F ` n ) } e. D -> E! e e. E { ( F ` m ) , ( F ` n ) } = ( F " e ) ) ) )
127 126 impl 
 |-  ( ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ ( a e. W /\ b e. W ) ) /\ m e. V ) /\ n e. V ) -> ( { ( F ` m ) , ( F ` n ) } e. D -> E! e e. E { ( F ` m ) , ( F ` n ) } = ( F " e ) ) )
128 eleq1 
 |-  ( d = { ( F ` m ) , ( F ` n ) } -> ( d e. D <-> { ( F ` m ) , ( F ` n ) } e. D ) )
129 eqeq1 
 |-  ( d = { ( F ` m ) , ( F ` n ) } -> ( d = ( F " e ) <-> { ( F ` m ) , ( F ` n ) } = ( F " e ) ) )
130 129 reubidv 
 |-  ( d = { ( F ` m ) , ( F ` n ) } -> ( E! e e. E d = ( F " e ) <-> E! e e. E { ( F ` m ) , ( F ` n ) } = ( F " e ) ) )
131 128 130 imbi12d 
 |-  ( d = { ( F ` m ) , ( F ` n ) } -> ( ( d e. D -> E! e e. E d = ( F " e ) ) <-> ( { ( F ` m ) , ( F ` n ) } e. D -> E! e e. E { ( F ` m ) , ( F ` n ) } = ( F " e ) ) ) )
132 127 131 syl5ibrcom 
 |-  ( ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ ( a e. W /\ b e. W ) ) /\ m e. V ) /\ n e. V ) -> ( d = { ( F ` m ) , ( F ` n ) } -> ( d e. D -> E! e e. E d = ( F " e ) ) ) )
133 132 adantr 
 |-  ( ( ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ ( a e. W /\ b e. W ) ) /\ m e. V ) /\ n e. V ) /\ ( b = ( F ` n ) /\ a = ( F ` m ) ) ) -> ( d = { ( F ` m ) , ( F ` n ) } -> ( d e. D -> E! e e. E d = ( F " e ) ) ) )
134 67 133 sylbid 
 |-  ( ( ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ ( a e. W /\ b e. W ) ) /\ m e. V ) /\ n e. V ) /\ ( b = ( F ` n ) /\ a = ( F ` m ) ) ) -> ( d = { a , b } -> ( d e. D -> E! e e. E d = ( F " e ) ) ) )
135 134 exp32 
 |-  ( ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ ( a e. W /\ b e. W ) ) /\ m e. V ) /\ n e. V ) -> ( b = ( F ` n ) -> ( a = ( F ` m ) -> ( d = { a , b } -> ( d e. D -> E! e e. E d = ( F " e ) ) ) ) ) )
136 135 rexlimdva 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ ( a e. W /\ b e. W ) ) /\ m e. V ) -> ( E. n e. V b = ( F ` n ) -> ( a = ( F ` m ) -> ( d = { a , b } -> ( d e. D -> E! e e. E d = ( F " e ) ) ) ) ) )
137 136 com23 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ ( a e. W /\ b e. W ) ) /\ m e. V ) -> ( a = ( F ` m ) -> ( E. n e. V b = ( F ` n ) -> ( d = { a , b } -> ( d e. D -> E! e e. E d = ( F " e ) ) ) ) ) )
138 137 rexlimdva 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ ( a e. W /\ b e. W ) ) -> ( E. m e. V a = ( F ` m ) -> ( E. n e. V b = ( F ` n ) -> ( d = { a , b } -> ( d e. D -> E! e e. E d = ( F " e ) ) ) ) ) )
139 138 impd 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ ( a e. W /\ b e. W ) ) -> ( ( E. m e. V a = ( F ` m ) /\ E. n e. V b = ( F ` n ) ) -> ( d = { a , b } -> ( d e. D -> E! e e. E d = ( F " e ) ) ) ) )
140 63 139 mpd 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ ( a e. W /\ b e. W ) ) -> ( d = { a , b } -> ( d e. D -> E! e e. E d = ( F " e ) ) ) )
141 140 com23 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ ( a e. W /\ b e. W ) ) -> ( d e. D -> ( d = { a , b } -> E! e e. E d = ( F " e ) ) ) )
142 141 impancom 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ d e. D ) -> ( ( a e. W /\ b e. W ) -> ( d = { a , b } -> E! e e. E d = ( F " e ) ) ) )
143 142 rexlimdvv 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ d e. D ) -> ( E. a e. W E. b e. W d = { a , b } -> E! e e. E d = ( F " e ) ) )
144 53 143 mpd 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) /\ d e. D ) -> E! e e. E d = ( F " e ) )
145 144 ralrimiva 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) -> A. d e. D E! e e. E d = ( F " e ) )
146 eqid 
 |-  ( e e. E |-> ( F " e ) ) = ( e e. E |-> ( F " e ) )
147 146 f1ompt 
 |-  ( ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D <-> ( A. e e. E ( F " e ) e. D /\ A. d e. D E! e e. E d = ( F " e ) ) )
148 49 145 147 sylanbrc 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) -> ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D )