Metamath Proof Explorer

Theorem uspgrlimlem3

Description: Lemma 3 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 uspgrlimlem3 
|- ( ( G e. USPGraph /\ h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> R /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) -> ( e e. K -> ( f " e ) = ( ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) ` e ) ) )

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 sseq1 
 |-  ( x = e -> ( x C_ N <-> e C_ N ) )
10 9 7 elrab2 
 |-  ( e e. K <-> ( e e. I /\ e C_ N ) )
11 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
12 11 uspgrf1oedg 
 |-  ( G e. USPGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-onto-> ( Edg ` G ) )
13 f1ocnv 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-onto-> ( Edg ` G ) -> `' ( iEdg ` G ) : ( Edg ` G ) -1-1-onto-> dom ( iEdg ` G ) )
14 f1of 
 |-  ( `' ( iEdg ` G ) : ( Edg ` G ) -1-1-onto-> dom ( iEdg ` G ) -> `' ( iEdg ` G ) : ( Edg ` G ) --> dom ( iEdg ` G ) )
15 12 13 14 3syl 
 |-  ( G e. USPGraph -> `' ( iEdg ` G ) : ( Edg ` G ) --> dom ( iEdg ` G ) )
16 15 3ad2ant1 
 |-  ( ( G e. USPGraph /\ h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> R /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) -> `' ( iEdg ` G ) : ( Edg ` G ) --> dom ( iEdg ` G ) )
17 5 eleq2i 
 |-  ( e e. I <-> e e. ( Edg ` G ) )
18 17 biimpi 
 |-  ( e e. I -> e e. ( Edg ` G ) )
19 18 adantr 
 |-  ( ( e e. I /\ e C_ N ) -> e e. ( Edg ` G ) )
20 fvco3 
 |-  ( ( `' ( iEdg ` G ) : ( Edg ` G ) --> dom ( iEdg ` G ) /\ e e. ( Edg ` G ) ) -> ( ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) ` e ) = ( ( ( iEdg ` H ) o. h ) ` ( `' ( iEdg ` G ) ` e ) ) )
21 16 19 20 syl2an 
 |-  ( ( ( G e. USPGraph /\ h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> R /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) /\ ( e e. I /\ e C_ N ) ) -> ( ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) ` e ) = ( ( ( iEdg ` H ) o. h ) ` ( `' ( iEdg ` G ) ` e ) ) )
22 f1ocnvdm 
 |-  ( ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-onto-> ( Edg ` G ) /\ e e. ( Edg ` G ) ) -> ( `' ( iEdg ` G ) ` e ) e. dom ( iEdg ` G ) )
23 12 19 22 syl2an 
 |-  ( ( G e. USPGraph /\ ( e e. I /\ e C_ N ) ) -> ( `' ( iEdg ` G ) ` e ) e. dom ( iEdg ` G ) )
24 f1ocnvfv2 
 |-  ( ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-onto-> ( Edg ` G ) /\ e e. ( Edg ` G ) ) -> ( ( iEdg ` G ) ` ( `' ( iEdg ` G ) ` e ) ) = e )
25 12 19 24 syl2an 
 |-  ( ( G e. USPGraph /\ ( e e. I /\ e C_ N ) ) -> ( ( iEdg ` G ) ` ( `' ( iEdg ` G ) ` e ) ) = e )
26 simprr 
 |-  ( ( G e. USPGraph /\ ( e e. I /\ e C_ N ) ) -> e C_ N )
27 25 26 eqsstrd 
 |-  ( ( G e. USPGraph /\ ( e e. I /\ e C_ N ) ) -> ( ( iEdg ` G ) ` ( `' ( iEdg ` G ) ` e ) ) C_ N )
28 23 27 jca 
 |-  ( ( G e. USPGraph /\ ( e e. I /\ e C_ N ) ) -> ( ( `' ( iEdg ` G ) ` e ) e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` ( `' ( iEdg ` G ) ` e ) ) C_ N ) )
29 28 adantlr 
 |-  ( ( ( G e. USPGraph /\ h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> R ) /\ ( e e. I /\ e C_ N ) ) -> ( ( `' ( iEdg ` G ) ` e ) e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` ( `' ( iEdg ` G ) ` e ) ) C_ N ) )
30 fveq2 
 |-  ( x = ( `' ( iEdg ` G ) ` e ) -> ( ( iEdg ` G ) ` x ) = ( ( iEdg ` G ) ` ( `' ( iEdg ` G ) ` e ) ) )
31 30 sseq1d 
 |-  ( x = ( `' ( iEdg ` G ) ` e ) -> ( ( ( iEdg ` G ) ` x ) C_ N <-> ( ( iEdg ` G ) ` ( `' ( iEdg ` G ) ` e ) ) C_ N ) )
32 31 elrab 
 |-  ( ( `' ( iEdg ` G ) ` e ) e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } <-> ( ( `' ( iEdg ` G ) ` e ) e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` ( `' ( iEdg ` G ) ` e ) ) C_ N ) )
33 29 32 sylibr 
 |-  ( ( ( G e. USPGraph /\ h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> R ) /\ ( e e. I /\ e C_ N ) ) -> ( `' ( iEdg ` G ) ` e ) e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } )
34 fveq2 
 |-  ( i = ( `' ( iEdg ` G ) ` e ) -> ( ( iEdg ` G ) ` i ) = ( ( iEdg ` G ) ` ( `' ( iEdg ` G ) ` e ) ) )
35 34 imaeq2d 
 |-  ( i = ( `' ( iEdg ` G ) ` e ) -> ( f " ( ( iEdg ` G ) ` i ) ) = ( f " ( ( iEdg ` G ) ` ( `' ( iEdg ` G ) ` e ) ) ) )
36 2fveq3 
 |-  ( i = ( `' ( iEdg ` G ) ` e ) -> ( ( iEdg ` H ) ` ( h ` i ) ) = ( ( iEdg ` H ) ` ( h ` ( `' ( iEdg ` G ) ` e ) ) ) )
37 35 36 eqeq12d 
 |-  ( i = ( `' ( iEdg ` G ) ` e ) -> ( ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) <-> ( f " ( ( iEdg ` G ) ` ( `' ( iEdg ` G ) ` e ) ) ) = ( ( iEdg ` H ) ` ( h ` ( `' ( iEdg ` G ) ` e ) ) ) ) )
38 37 rspcv 
 |-  ( ( `' ( iEdg ` G ) ` e ) e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -> ( A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) -> ( f " ( ( iEdg ` G ) ` ( `' ( iEdg ` G ) ` e ) ) ) = ( ( iEdg ` H ) ` ( h ` ( `' ( iEdg ` G ) ` e ) ) ) ) )
39 33 38 syl 
 |-  ( ( ( G e. USPGraph /\ h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> R ) /\ ( e e. I /\ e C_ N ) ) -> ( A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) -> ( f " ( ( iEdg ` G ) ` ( `' ( iEdg ` G ) ` e ) ) ) = ( ( iEdg ` H ) ` ( h ` ( `' ( iEdg ` G ) ` e ) ) ) ) )
40 eqcom 
 |-  ( ( f " ( ( iEdg ` G ) ` ( `' ( iEdg ` G ) ` e ) ) ) = ( ( iEdg ` H ) ` ( h ` ( `' ( iEdg ` G ) ` e ) ) ) <-> ( ( iEdg ` H ) ` ( h ` ( `' ( iEdg ` G ) ` e ) ) ) = ( f " ( ( iEdg ` G ) ` ( `' ( iEdg ` G ) ` e ) ) ) )
41 f1of 
 |-  ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> R -> h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } --> R )
42 41 ad2antlr 
 |-  ( ( ( G e. USPGraph /\ h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> R ) /\ ( e e. I /\ e C_ N ) ) -> h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } --> R )
43 42 33 fvco3d 
 |-  ( ( ( G e. USPGraph /\ h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> R ) /\ ( e e. I /\ e C_ N ) ) -> ( ( ( iEdg ` H ) o. h ) ` ( `' ( iEdg ` G ) ` e ) ) = ( ( iEdg ` H ) ` ( h ` ( `' ( iEdg ` G ) ` e ) ) ) )
44 43 eqcomd 
 |-  ( ( ( G e. USPGraph /\ h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> R ) /\ ( e e. I /\ e C_ N ) ) -> ( ( iEdg ` H ) ` ( h ` ( `' ( iEdg ` G ) ` e ) ) ) = ( ( ( iEdg ` H ) o. h ) ` ( `' ( iEdg ` G ) ` e ) ) )
45 12 adantr 
 |-  ( ( G e. USPGraph /\ h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> R ) -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-onto-> ( Edg ` G ) )
46 45 19 24 syl2an 
 |-  ( ( ( G e. USPGraph /\ h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> R ) /\ ( e e. I /\ e C_ N ) ) -> ( ( iEdg ` G ) ` ( `' ( iEdg ` G ) ` e ) ) = e )
47 46 imaeq2d 
 |-  ( ( ( G e. USPGraph /\ h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> R ) /\ ( e e. I /\ e C_ N ) ) -> ( f " ( ( iEdg ` G ) ` ( `' ( iEdg ` G ) ` e ) ) ) = ( f " e ) )
48 44 47 eqeq12d 
 |-  ( ( ( G e. USPGraph /\ h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> R ) /\ ( e e. I /\ e C_ N ) ) -> ( ( ( iEdg ` H ) ` ( h ` ( `' ( iEdg ` G ) ` e ) ) ) = ( f " ( ( iEdg ` G ) ` ( `' ( iEdg ` G ) ` e ) ) ) <-> ( ( ( iEdg ` H ) o. h ) ` ( `' ( iEdg ` G ) ` e ) ) = ( f " e ) ) )
49 48 biimpd 
 |-  ( ( ( G e. USPGraph /\ h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> R ) /\ ( e e. I /\ e C_ N ) ) -> ( ( ( iEdg ` H ) ` ( h ` ( `' ( iEdg ` G ) ` e ) ) ) = ( f " ( ( iEdg ` G ) ` ( `' ( iEdg ` G ) ` e ) ) ) -> ( ( ( iEdg ` H ) o. h ) ` ( `' ( iEdg ` G ) ` e ) ) = ( f " e ) ) )
50 40 49 biimtrid 
 |-  ( ( ( G e. USPGraph /\ h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> R ) /\ ( e e. I /\ e C_ N ) ) -> ( ( f " ( ( iEdg ` G ) ` ( `' ( iEdg ` G ) ` e ) ) ) = ( ( iEdg ` H ) ` ( h ` ( `' ( iEdg ` G ) ` e ) ) ) -> ( ( ( iEdg ` H ) o. h ) ` ( `' ( iEdg ` G ) ` e ) ) = ( f " e ) ) )
51 39 50 syld 
 |-  ( ( ( G e. USPGraph /\ h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> R ) /\ ( e e. I /\ e C_ N ) ) -> ( A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) -> ( ( ( iEdg ` H ) o. h ) ` ( `' ( iEdg ` G ) ` e ) ) = ( f " e ) ) )
52 51 ex 
 |-  ( ( G e. USPGraph /\ h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> R ) -> ( ( e e. I /\ e C_ N ) -> ( A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) -> ( ( ( iEdg ` H ) o. h ) ` ( `' ( iEdg ` G ) ` e ) ) = ( f " e ) ) ) )
53 52 com23 
 |-  ( ( G e. USPGraph /\ h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> R ) -> ( A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) -> ( ( e e. I /\ e C_ N ) -> ( ( ( iEdg ` H ) o. h ) ` ( `' ( iEdg ` G ) ` e ) ) = ( f " e ) ) ) )
54 53 ex 
 |-  ( G e. USPGraph -> ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> R -> ( A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) -> ( ( e e. I /\ e C_ N ) -> ( ( ( iEdg ` H ) o. h ) ` ( `' ( iEdg ` G ) ` e ) ) = ( f " e ) ) ) ) )
55 54 3imp1 
 |-  ( ( ( G e. USPGraph /\ h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> R /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) /\ ( e e. I /\ e C_ N ) ) -> ( ( ( iEdg ` H ) o. h ) ` ( `' ( iEdg ` G ) ` e ) ) = ( f " e ) )
56 21 55 eqtr2d 
 |-  ( ( ( G e. USPGraph /\ h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> R /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) /\ ( e e. I /\ e C_ N ) ) -> ( f " e ) = ( ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) ` e ) )
57 56 ex 
 |-  ( ( G e. USPGraph /\ h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> R /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) -> ( ( e e. I /\ e C_ N ) -> ( f " e ) = ( ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) ` e ) ) )
58 10 57 biimtrid 
 |-  ( ( G e. USPGraph /\ h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> R /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) -> ( e e. K -> ( f " e ) = ( ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) ` e ) ) )