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 birani 
 |-  ( ( e e. I /\ e C_ N ) -> e e. ( Edg ` G ) )
19 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 ) ) )
20 16 18 19 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 ) ) )
21 f1ocnvdm 
 |-  ( ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-onto-> ( Edg ` G ) /\ e e. ( Edg ` G ) ) -> ( `' ( iEdg ` G ) ` e ) e. dom ( iEdg ` G ) )
22 12 18 21 syl2an 
 |-  ( ( G e. USPGraph /\ ( e e. I /\ e C_ N ) ) -> ( `' ( iEdg ` G ) ` e ) e. dom ( iEdg ` G ) )
23 f1ocnvfv2 
 |-  ( ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-onto-> ( Edg ` G ) /\ e e. ( Edg ` G ) ) -> ( ( iEdg ` G ) ` ( `' ( iEdg ` G ) ` e ) ) = e )
24 12 18 23 syl2an 
 |-  ( ( G e. USPGraph /\ ( e e. I /\ e C_ N ) ) -> ( ( iEdg ` G ) ` ( `' ( iEdg ` G ) ` e ) ) = e )
25 simprr 
 |-  ( ( G e. USPGraph /\ ( e e. I /\ e C_ N ) ) -> e C_ N )
26 24 25 eqsstrd 
 |-  ( ( G e. USPGraph /\ ( e e. I /\ e C_ N ) ) -> ( ( iEdg ` G ) ` ( `' ( iEdg ` G ) ` e ) ) C_ N )
27 22 26 jca 
 |-  ( ( G e. USPGraph /\ ( e e. I /\ e C_ N ) ) -> ( ( `' ( iEdg ` G ) ` e ) e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` ( `' ( iEdg ` G ) ` e ) ) C_ N ) )
28 27 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 ) )
29 fveq2 
 |-  ( x = ( `' ( iEdg ` G ) ` e ) -> ( ( iEdg ` G ) ` x ) = ( ( iEdg ` G ) ` ( `' ( iEdg ` G ) ` e ) ) )
30 29 sseq1d 
 |-  ( x = ( `' ( iEdg ` G ) ` e ) -> ( ( ( iEdg ` G ) ` x ) C_ N <-> ( ( iEdg ` G ) ` ( `' ( iEdg ` G ) ` e ) ) C_ N ) )
31 30 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 ) )
32 28 31 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 } )
33 fveq2 
 |-  ( i = ( `' ( iEdg ` G ) ` e ) -> ( ( iEdg ` G ) ` i ) = ( ( iEdg ` G ) ` ( `' ( iEdg ` G ) ` e ) ) )
34 33 imaeq2d 
 |-  ( i = ( `' ( iEdg ` G ) ` e ) -> ( f " ( ( iEdg ` G ) ` i ) ) = ( f " ( ( iEdg ` G ) ` ( `' ( iEdg ` G ) ` e ) ) ) )
35 2fveq3 
 |-  ( i = ( `' ( iEdg ` G ) ` e ) -> ( ( iEdg ` H ) ` ( h ` i ) ) = ( ( iEdg ` H ) ` ( h ` ( `' ( iEdg ` G ) ` e ) ) ) )
36 34 35 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 ) ) ) ) )
37 36 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 ) ) ) ) )
38 32 37 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 ) ) ) ) )
39 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 ) ) ) )
40 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 )
41 40 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 )
42 41 32 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 ) ) ) )
43 42 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 ) ) )
44 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 ) )
45 44 18 23 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 )
46 45 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 ) )
47 43 46 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 ) ) )
48 47 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 ) ) )
49 39 48 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 ) ) )
50 38 49 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 ) ) )
51 50 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 ) ) ) )
52 51 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 ) ) ) )
53 52 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 ) ) ) ) )
54 53 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 ) )
55 20 54 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 ) )
56 55 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 ) ) )
57 10 56 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 ) ) )