Metamath Proof Explorer

Theorem uspgrlimlem4

Description: Lemma 4 for uspgrlim . (Contributed by AV, 16-Aug-2025)

Ref Expression
Hypotheses uspgrlim.v 
|- V = ( Vtx ` G )
uspgrlim.w 
|- W = ( Vtx ` H )
uspgrlim.n 
|- N = ( G ClNeighbVtx v )
uspgrlim.m 
|- M = ( H ClNeighbVtx ( F ` v ) )
uspgrlim.i 
|- I = ( Edg ` G )
uspgrlim.j 
|- J = ( Edg ` H )
uspgrlim.k 
|- K = { x e. I | x C_ N }
uspgrlim.l 
|- L = { x e. J | x C_ M }
Assertion uspgrlimlem4 
|- ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) -> ( ( i e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` i ) C_ N ) -> ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) ` i ) ) ) )

Proof

Step Hyp Ref Expression
1 uspgrlim.v 
 |-  V = ( Vtx ` G )
2 uspgrlim.w 
 |-  W = ( Vtx ` H )
3 uspgrlim.n 
 |-  N = ( G ClNeighbVtx v )
4 uspgrlim.m 
 |-  M = ( H ClNeighbVtx ( F ` v ) )
5 uspgrlim.i 
 |-  I = ( Edg ` G )
6 uspgrlim.j 
 |-  J = ( Edg ` H )
7 uspgrlim.k 
 |-  K = { x e. I | x C_ N }
8 uspgrlim.l 
 |-  L = { x e. J | x C_ M }
9 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
10 9 uspgrf1oedg 
 |-  ( G e. USPGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-onto-> ( Edg ` G ) )
11 f1of 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-onto-> ( Edg ` G ) -> ( iEdg ` G ) : dom ( iEdg ` G ) --> ( Edg ` G ) )
12 10 11 syl 
 |-  ( G e. USPGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) --> ( Edg ` G ) )
13 12 ad2antrr 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) -> ( iEdg ` G ) : dom ( iEdg ` G ) --> ( Edg ` G ) )
14 simpl 
 |-  ( ( i e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` i ) C_ N ) -> i e. dom ( iEdg ` G ) )
15 fvco3 
 |-  ( ( ( iEdg ` G ) : dom ( iEdg ` G ) --> ( Edg ` G ) /\ i e. dom ( iEdg ` G ) ) -> ( ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) ` i ) = ( ( `' ( iEdg ` H ) o. g ) ` ( ( iEdg ` G ) ` i ) ) )
16 15 fveq2d 
 |-  ( ( ( iEdg ` G ) : dom ( iEdg ` G ) --> ( Edg ` G ) /\ i e. dom ( iEdg ` G ) ) -> ( ( iEdg ` H ) ` ( ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) ` i ) ) = ( ( iEdg ` H ) ` ( ( `' ( iEdg ` H ) o. g ) ` ( ( iEdg ` G ) ` i ) ) ) )
17 13 14 16 syl2an 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) /\ ( i e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` i ) C_ N ) ) -> ( ( iEdg ` H ) ` ( ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) ` i ) ) = ( ( iEdg ` H ) ` ( ( `' ( iEdg ` H ) o. g ) ` ( ( iEdg ` G ) ` i ) ) ) )
18 eqid 
 |-  ( iEdg ` H ) = ( iEdg ` H )
19 18 uspgrf1oedg 
 |-  ( H e. USPGraph -> ( iEdg ` H ) : dom ( iEdg ` H ) -1-1-onto-> ( Edg ` H ) )
20 19 ad3antlr 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) /\ ( i e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` i ) C_ N ) ) -> ( iEdg ` H ) : dom ( iEdg ` H ) -1-1-onto-> ( Edg ` H ) )
21 ssrab2 
 |-  { x e. J | x C_ M } C_ J
22 6 eqcomi 
 |-  ( Edg ` H ) = J
23 21 8 22 3sstr4i 
 |-  L C_ ( Edg ` H )
24 f1of 
 |-  ( g : K -1-1-onto-> L -> g : K --> L )
25 24 adantr 
 |-  ( ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) -> g : K --> L )
26 25 adantl 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) -> g : K --> L )
27 26 adantr 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) /\ ( i e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` i ) C_ N ) ) -> g : K --> L )
28 13 ffund 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) -> Fun ( iEdg ` G ) )
29 9 iedgedg 
 |-  ( ( Fun ( iEdg ` G ) /\ i e. dom ( iEdg ` G ) ) -> ( ( iEdg ` G ) ` i ) e. ( Edg ` G ) )
30 28 14 29 syl2an 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) /\ ( i e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` i ) C_ N ) ) -> ( ( iEdg ` G ) ` i ) e. ( Edg ` G ) )
31 30 5 eleqtrrdi 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) /\ ( i e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` i ) C_ N ) ) -> ( ( iEdg ` G ) ` i ) e. I )
32 simprr 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) /\ ( i e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` i ) C_ N ) ) -> ( ( iEdg ` G ) ` i ) C_ N )
33 sseq1 
 |-  ( x = ( ( iEdg ` G ) ` i ) -> ( x C_ N <-> ( ( iEdg ` G ) ` i ) C_ N ) )
34 33 7 elrab2 
 |-  ( ( ( iEdg ` G ) ` i ) e. K <-> ( ( ( iEdg ` G ) ` i ) e. I /\ ( ( iEdg ` G ) ` i ) C_ N ) )
35 31 32 34 sylanbrc 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) /\ ( i e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` i ) C_ N ) ) -> ( ( iEdg ` G ) ` i ) e. K )
36 27 35 ffvelcdmd 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) /\ ( i e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` i ) C_ N ) ) -> ( g ` ( ( iEdg ` G ) ` i ) ) e. L )
37 23 36 sselid 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) /\ ( i e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` i ) C_ N ) ) -> ( g ` ( ( iEdg ` G ) ` i ) ) e. ( Edg ` H ) )
38 f1ocnvfv2 
 |-  ( ( ( iEdg ` H ) : dom ( iEdg ` H ) -1-1-onto-> ( Edg ` H ) /\ ( g ` ( ( iEdg ` G ) ` i ) ) e. ( Edg ` H ) ) -> ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` ( g ` ( ( iEdg ` G ) ` i ) ) ) ) = ( g ` ( ( iEdg ` G ) ` i ) ) )
39 20 37 38 syl2anc 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) /\ ( i e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` i ) C_ N ) ) -> ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` ( g ` ( ( iEdg ` G ) ` i ) ) ) ) = ( g ` ( ( iEdg ` G ) ` i ) ) )
40 fvco3 
 |-  ( ( g : K --> L /\ ( ( iEdg ` G ) ` i ) e. K ) -> ( ( `' ( iEdg ` H ) o. g ) ` ( ( iEdg ` G ) ` i ) ) = ( `' ( iEdg ` H ) ` ( g ` ( ( iEdg ` G ) ` i ) ) ) )
41 40 fveq2d 
 |-  ( ( g : K --> L /\ ( ( iEdg ` G ) ` i ) e. K ) -> ( ( iEdg ` H ) ` ( ( `' ( iEdg ` H ) o. g ) ` ( ( iEdg ` G ) ` i ) ) ) = ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` ( g ` ( ( iEdg ` G ) ` i ) ) ) ) )
42 27 35 41 syl2anc 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) /\ ( i e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` i ) C_ N ) ) -> ( ( iEdg ` H ) ` ( ( `' ( iEdg ` H ) o. g ) ` ( ( iEdg ` G ) ` i ) ) ) = ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` ( g ` ( ( iEdg ` G ) ` i ) ) ) ) )
43 5 eqcomi 
 |-  ( Edg ` G ) = I
44 feq3 
 |-  ( ( Edg ` G ) = I -> ( ( iEdg ` G ) : dom ( iEdg ` G ) --> ( Edg ` G ) <-> ( iEdg ` G ) : dom ( iEdg ` G ) --> I ) )
45 43 44 ax-mp 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) --> ( Edg ` G ) <-> ( iEdg ` G ) : dom ( iEdg ` G ) --> I )
46 45 biimpi 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) --> ( Edg ` G ) -> ( iEdg ` G ) : dom ( iEdg ` G ) --> I )
47 10 11 46 3syl 
 |-  ( G e. USPGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) --> I )
48 47 ad2antrr 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( i e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` i ) C_ N ) ) -> ( iEdg ` G ) : dom ( iEdg ` G ) --> I )
49 14 adantl 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( i e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` i ) C_ N ) ) -> i e. dom ( iEdg ` G ) )
50 48 49 ffvelcdmd 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( i e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` i ) C_ N ) ) -> ( ( iEdg ` G ) ` i ) e. I )
51 simprr 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( i e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` i ) C_ N ) ) -> ( ( iEdg ` G ) ` i ) C_ N )
52 50 51 34 sylanbrc 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( i e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` i ) C_ N ) ) -> ( ( iEdg ` G ) ` i ) e. K )
53 imaeq2 
 |-  ( e = ( ( iEdg ` G ) ` i ) -> ( f " e ) = ( f " ( ( iEdg ` G ) ` i ) ) )
54 fveq2 
 |-  ( e = ( ( iEdg ` G ) ` i ) -> ( g ` e ) = ( g ` ( ( iEdg ` G ) ` i ) ) )
55 53 54 eqeq12d 
 |-  ( e = ( ( iEdg ` G ) ` i ) -> ( ( f " e ) = ( g ` e ) <-> ( f " ( ( iEdg ` G ) ` i ) ) = ( g ` ( ( iEdg ` G ) ` i ) ) ) )
56 55 rspcv 
 |-  ( ( ( iEdg ` G ) ` i ) e. K -> ( A. e e. K ( f " e ) = ( g ` e ) -> ( f " ( ( iEdg ` G ) ` i ) ) = ( g ` ( ( iEdg ` G ) ` i ) ) ) )
57 52 56 syl 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( i e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` i ) C_ N ) ) -> ( A. e e. K ( f " e ) = ( g ` e ) -> ( f " ( ( iEdg ` G ) ` i ) ) = ( g ` ( ( iEdg ` G ) ` i ) ) ) )
58 57 ex 
 |-  ( ( G e. USPGraph /\ H e. USPGraph ) -> ( ( i e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` i ) C_ N ) -> ( A. e e. K ( f " e ) = ( g ` e ) -> ( f " ( ( iEdg ` G ) ` i ) ) = ( g ` ( ( iEdg ` G ) ` i ) ) ) ) )
59 58 com23 
 |-  ( ( G e. USPGraph /\ H e. USPGraph ) -> ( A. e e. K ( f " e ) = ( g ` e ) -> ( ( i e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` i ) C_ N ) -> ( f " ( ( iEdg ` G ) ` i ) ) = ( g ` ( ( iEdg ` G ) ` i ) ) ) ) )
60 59 adantld 
 |-  ( ( G e. USPGraph /\ H e. USPGraph ) -> ( ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) -> ( ( i e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` i ) C_ N ) -> ( f " ( ( iEdg ` G ) ` i ) ) = ( g ` ( ( iEdg ` G ) ` i ) ) ) ) )
61 60 imp31 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) /\ ( i e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` i ) C_ N ) ) -> ( f " ( ( iEdg ` G ) ` i ) ) = ( g ` ( ( iEdg ` G ) ` i ) ) )
62 39 42 61 3eqtr4d 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) /\ ( i e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` i ) C_ N ) ) -> ( ( iEdg ` H ) ` ( ( `' ( iEdg ` H ) o. g ) ` ( ( iEdg ` G ) ` i ) ) ) = ( f " ( ( iEdg ` G ) ` i ) ) )
63 17 62 eqtr2d 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) /\ ( i e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` i ) C_ N ) ) -> ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) ` i ) ) )
64 63 ex 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) -> ( ( i e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` i ) C_ N ) -> ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) ` i ) ) ) )