This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uhgrimedgi

Description: An isomorphism between graphs preserves edges, i.e. if there is an edge in one graph connecting vertices then there is an edge in the other graph connecting the corresponding vertices. (Contributed by AV, 25-Oct-2025)

Ref Expression
Hypotheses uhgrimedgi.e 
|- E = ( Edg ` G )
uhgrimedgi.d 
|- D = ( Edg ` H )
Assertion uhgrimedgi 
|- ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ ( F e. ( G GraphIso H ) /\ K e. E ) ) -> ( F " K ) e. D )

Proof

Step Hyp Ref Expression
1 uhgrimedgi.e 
 |-  E = ( Edg ` G )
2 uhgrimedgi.d 
 |-  D = ( Edg ` H )
3 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
4 eqid 
 |-  ( Vtx ` H ) = ( Vtx ` H )
5 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
6 eqid 
 |-  ( iEdg ` H ) = ( iEdg ` H )
7 3 4 5 6 grimprop 
 |-  ( F e. ( G GraphIso H ) -> ( F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) /\ E. j ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) )
8 1 eleq2i 
 |-  ( K e. E <-> K e. ( Edg ` G ) )
9 5 uhgrfun 
 |-  ( G e. UHGraph -> Fun ( iEdg ` G ) )
10 5 edgiedgb 
 |-  ( Fun ( iEdg ` G ) -> ( K e. ( Edg ` G ) <-> E. k e. dom ( iEdg ` G ) K = ( ( iEdg ` G ) ` k ) ) )
11 9 10 syl 
 |-  ( G e. UHGraph -> ( K e. ( Edg ` G ) <-> E. k e. dom ( iEdg ` G ) K = ( ( iEdg ` G ) ` k ) ) )
12 8 11 bitrid 
 |-  ( G e. UHGraph -> ( K e. E <-> E. k e. dom ( iEdg ` G ) K = ( ( iEdg ` G ) ` k ) ) )
13 12 adantr 
 |-  ( ( G e. UHGraph /\ H e. UHGraph ) -> ( K e. E <-> E. k e. dom ( iEdg ` G ) K = ( ( iEdg ` G ) ` k ) ) )
14 simplr 
 |-  ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) -> k e. dom ( iEdg ` G ) )
15 2fveq3 
 |-  ( i = k -> ( ( iEdg ` H ) ` ( j ` i ) ) = ( ( iEdg ` H ) ` ( j ` k ) ) )
16 fveq2 
 |-  ( i = k -> ( ( iEdg ` G ) ` i ) = ( ( iEdg ` G ) ` k ) )
17 16 imaeq2d 
 |-  ( i = k -> ( F " ( ( iEdg ` G ) ` i ) ) = ( F " ( ( iEdg ` G ) ` k ) ) )
18 15 17 eqeq12d 
 |-  ( i = k -> ( ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) <-> ( ( iEdg ` H ) ` ( j ` k ) ) = ( F " ( ( iEdg ` G ) ` k ) ) ) )
19 18 rspcv 
 |-  ( k e. dom ( iEdg ` G ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( ( iEdg ` H ) ` ( j ` k ) ) = ( F " ( ( iEdg ` G ) ` k ) ) ) )
20 14 19 syl 
 |-  ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( ( iEdg ` H ) ` ( j ` k ) ) = ( F " ( ( iEdg ` G ) ` k ) ) ) )
21 6 uhgrfun 
 |-  ( H e. UHGraph -> Fun ( iEdg ` H ) )
22 21 ad3antlr 
 |-  ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) -> Fun ( iEdg ` H ) )
23 f1of 
 |-  ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) -> j : dom ( iEdg ` G ) --> dom ( iEdg ` H ) )
24 23 adantl 
 |-  ( ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) -> j : dom ( iEdg ` G ) --> dom ( iEdg ` H ) )
25 14 adantr 
 |-  ( ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) -> k e. dom ( iEdg ` G ) )
26 24 25 ffvelcdmd 
 |-  ( ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) -> ( j ` k ) e. dom ( iEdg ` H ) )
27 6 iedgedg 
 |-  ( ( Fun ( iEdg ` H ) /\ ( j ` k ) e. dom ( iEdg ` H ) ) -> ( ( iEdg ` H ) ` ( j ` k ) ) e. ( Edg ` H ) )
28 22 26 27 syl2an2r 
 |-  ( ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) -> ( ( iEdg ` H ) ` ( j ` k ) ) e. ( Edg ` H ) )
29 28 2 eleqtrrdi 
 |-  ( ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) -> ( ( iEdg ` H ) ` ( j ` k ) ) e. D )
30 eleq1 
 |-  ( ( F " ( ( iEdg ` G ) ` k ) ) = ( ( iEdg ` H ) ` ( j ` k ) ) -> ( ( F " ( ( iEdg ` G ) ` k ) ) e. D <-> ( ( iEdg ` H ) ` ( j ` k ) ) e. D ) )
31 30 eqcoms 
 |-  ( ( ( iEdg ` H ) ` ( j ` k ) ) = ( F " ( ( iEdg ` G ) ` k ) ) -> ( ( F " ( ( iEdg ` G ) ` k ) ) e. D <-> ( ( iEdg ` H ) ` ( j ` k ) ) e. D ) )
32 29 31 syl5ibrcom 
 |-  ( ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) -> ( ( ( iEdg ` H ) ` ( j ` k ) ) = ( F " ( ( iEdg ` G ) ` k ) ) -> ( F " ( ( iEdg ` G ) ` k ) ) e. D ) )
33 32 ex 
 |-  ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) -> ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) -> ( ( ( iEdg ` H ) ` ( j ` k ) ) = ( F " ( ( iEdg ` G ) ` k ) ) -> ( F " ( ( iEdg ` G ) ` k ) ) e. D ) ) )
34 20 33 syl5d 
 |-  ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) -> ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( F " ( ( iEdg ` G ) ` k ) ) e. D ) ) )
35 34 impd 
 |-  ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) -> ( ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> ( F " ( ( iEdg ` G ) ` k ) ) e. D ) )
36 35 ex 
 |-  ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) -> ( F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) -> ( ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> ( F " ( ( iEdg ` G ) ` k ) ) e. D ) ) )
37 36 adantr 
 |-  ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) /\ K = ( ( iEdg ` G ) ` k ) ) -> ( F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) -> ( ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> ( F " ( ( iEdg ` G ) ` k ) ) e. D ) ) )
38 37 3imp 
 |-  ( ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) /\ K = ( ( iEdg ` G ) ` k ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) -> ( F " ( ( iEdg ` G ) ` k ) ) e. D )
39 imaeq2 
 |-  ( K = ( ( iEdg ` G ) ` k ) -> ( F " K ) = ( F " ( ( iEdg ` G ) ` k ) ) )
40 39 eleq1d 
 |-  ( K = ( ( iEdg ` G ) ` k ) -> ( ( F " K ) e. D <-> ( F " ( ( iEdg ` G ) ` k ) ) e. D ) )
41 40 adantl 
 |-  ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) /\ K = ( ( iEdg ` G ) ` k ) ) -> ( ( F " K ) e. D <-> ( F " ( ( iEdg ` G ) ` k ) ) e. D ) )
42 41 3ad2ant1 
 |-  ( ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) /\ K = ( ( iEdg ` G ) ` k ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) -> ( ( F " K ) e. D <-> ( F " ( ( iEdg ` G ) ` k ) ) e. D ) )
43 38 42 mpbird 
 |-  ( ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) /\ K = ( ( iEdg ` G ) ` k ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) -> ( F " K ) e. D )
44 43 3exp 
 |-  ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) /\ K = ( ( iEdg ` G ) ` k ) ) -> ( F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) -> ( ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> ( F " K ) e. D ) ) )
45 44 ex 
 |-  ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) -> ( K = ( ( iEdg ` G ) ` k ) -> ( F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) -> ( ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> ( F " K ) e. D ) ) ) )
46 45 rexlimdva 
 |-  ( ( G e. UHGraph /\ H e. UHGraph ) -> ( E. k e. dom ( iEdg ` G ) K = ( ( iEdg ` G ) ` k ) -> ( F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) -> ( ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> ( F " K ) e. D ) ) ) )
47 13 46 sylbid 
 |-  ( ( G e. UHGraph /\ H e. UHGraph ) -> ( K e. E -> ( F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) -> ( ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> ( F " K ) e. D ) ) ) )
48 47 imp 
 |-  ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ K e. E ) -> ( F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) -> ( ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> ( F " K ) e. D ) ) )
49 48 imp 
 |-  ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ K e. E ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) -> ( ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> ( F " K ) e. D ) )
50 49 exlimdv 
 |-  ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ K e. E ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) -> ( E. j ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> ( F " K ) e. D ) )
51 50 expimpd 
 |-  ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ K e. E ) -> ( ( F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) /\ E. j ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) -> ( F " K ) e. D ) )
52 7 51 syl5 
 |-  ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ K e. E ) -> ( F e. ( G GraphIso H ) -> ( F " K ) e. D ) )
53 52 ex 
 |-  ( ( G e. UHGraph /\ H e. UHGraph ) -> ( K e. E -> ( F e. ( G GraphIso H ) -> ( F " K ) e. D ) ) )
54 53 impcomd 
 |-  ( ( G e. UHGraph /\ H e. UHGraph ) -> ( ( F e. ( G GraphIso H ) /\ K e. E ) -> ( F " K ) e. D ) )
55 54 imp 
 |-  ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ ( F e. ( G GraphIso H ) /\ K e. E ) ) -> ( F " K ) e. D )