Metamath Proof Explorer

Theorem uspgrlimlem2

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

Ref Expression
Hypotheses uspgrlimlem1.m 
|- M = ( H ClNeighbVtx X )
uspgrlimlem1.j 
|- J = ( Edg ` H )
uspgrlimlem1.l 
|- L = { x e. J | x C_ M }
Assertion uspgrlimlem2 
|- ( H e. USPGraph -> ( `' ( iEdg ` H ) " L ) = { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } )

Proof

Step Hyp Ref Expression
1 uspgrlimlem1.m 
 |-  M = ( H ClNeighbVtx X )
2 uspgrlimlem1.j 
 |-  J = ( Edg ` H )
3 uspgrlimlem1.l 
 |-  L = { x e. J | x C_ M }
4 eqid 
 |-  ( iEdg ` H ) = ( iEdg ` H )
5 4 uspgrf1oedg 
 |-  ( H e. USPGraph -> ( iEdg ` H ) : dom ( iEdg ` H ) -1-1-onto-> ( Edg ` H ) )
6 f1ocnv 
 |-  ( ( iEdg ` H ) : dom ( iEdg ` H ) -1-1-onto-> ( Edg ` H ) -> `' ( iEdg ` H ) : ( Edg ` H ) -1-1-onto-> dom ( iEdg ` H ) )
7 f1of 
 |-  ( `' ( iEdg ` H ) : ( Edg ` H ) -1-1-onto-> dom ( iEdg ` H ) -> `' ( iEdg ` H ) : ( Edg ` H ) --> dom ( iEdg ` H ) )
8 5 6 7 3syl 
 |-  ( H e. USPGraph -> `' ( iEdg ` H ) : ( Edg ` H ) --> dom ( iEdg ` H ) )
9 2 rabeqi 
 |-  { x e. J | x C_ M } = { x e. ( Edg ` H ) | x C_ M }
10 3 9 eqtri 
 |-  L = { x e. ( Edg ` H ) | x C_ M }
11 10 ssrab3 
 |-  L C_ ( Edg ` H )
12 fimarab 
 |-  ( ( `' ( iEdg ` H ) : ( Edg ` H ) --> dom ( iEdg ` H ) /\ L C_ ( Edg ` H ) ) -> ( `' ( iEdg ` H ) " L ) = { x e. dom ( iEdg ` H ) | E. y e. L ( `' ( iEdg ` H ) ` y ) = x } )
13 8 11 12 sylancl 
 |-  ( H e. USPGraph -> ( `' ( iEdg ` H ) " L ) = { x e. dom ( iEdg ` H ) | E. y e. L ( `' ( iEdg ` H ) ` y ) = x } )
14 sseq1 
 |-  ( x = y -> ( x C_ M <-> y C_ M ) )
15 14 3 elrab2 
 |-  ( y e. L <-> ( y e. J /\ y C_ M ) )
16 2 eleq2i 
 |-  ( y e. J <-> y e. ( Edg ` H ) )
17 16 biimpi 
 |-  ( y e. J -> y e. ( Edg ` H ) )
18 f1ocnvfv2 
 |-  ( ( ( iEdg ` H ) : dom ( iEdg ` H ) -1-1-onto-> ( Edg ` H ) /\ y e. ( Edg ` H ) ) -> ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) = y )
19 5 17 18 syl2an 
 |-  ( ( H e. USPGraph /\ y e. J ) -> ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) = y )
20 19 eqcomd 
 |-  ( ( H e. USPGraph /\ y e. J ) -> y = ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) )
21 20 sseq1d 
 |-  ( ( H e. USPGraph /\ y e. J ) -> ( y C_ M <-> ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) C_ M ) )
22 21 biimpd 
 |-  ( ( H e. USPGraph /\ y e. J ) -> ( y C_ M -> ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) C_ M ) )
23 22 ex 
 |-  ( H e. USPGraph -> ( y e. J -> ( y C_ M -> ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) C_ M ) ) )
24 23 adantr 
 |-  ( ( H e. USPGraph /\ x e. dom ( iEdg ` H ) ) -> ( y e. J -> ( y C_ M -> ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) C_ M ) ) )
25 24 imp32 
 |-  ( ( ( H e. USPGraph /\ x e. dom ( iEdg ` H ) ) /\ ( y e. J /\ y C_ M ) ) -> ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) C_ M )
26 25 3adant3 
 |-  ( ( ( H e. USPGraph /\ x e. dom ( iEdg ` H ) ) /\ ( y e. J /\ y C_ M ) /\ ( `' ( iEdg ` H ) ` y ) = x ) -> ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) C_ M )
27 fveq2 
 |-  ( ( `' ( iEdg ` H ) ` y ) = x -> ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) = ( ( iEdg ` H ) ` x ) )
28 27 sseq1d 
 |-  ( ( `' ( iEdg ` H ) ` y ) = x -> ( ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) C_ M <-> ( ( iEdg ` H ) ` x ) C_ M ) )
29 28 3ad2ant3 
 |-  ( ( ( H e. USPGraph /\ x e. dom ( iEdg ` H ) ) /\ ( y e. J /\ y C_ M ) /\ ( `' ( iEdg ` H ) ` y ) = x ) -> ( ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) C_ M <-> ( ( iEdg ` H ) ` x ) C_ M ) )
30 26 29 mpbid 
 |-  ( ( ( H e. USPGraph /\ x e. dom ( iEdg ` H ) ) /\ ( y e. J /\ y C_ M ) /\ ( `' ( iEdg ` H ) ` y ) = x ) -> ( ( iEdg ` H ) ` x ) C_ M )
31 30 3exp 
 |-  ( ( H e. USPGraph /\ x e. dom ( iEdg ` H ) ) -> ( ( y e. J /\ y C_ M ) -> ( ( `' ( iEdg ` H ) ` y ) = x -> ( ( iEdg ` H ) ` x ) C_ M ) ) )
32 15 31 biimtrid 
 |-  ( ( H e. USPGraph /\ x e. dom ( iEdg ` H ) ) -> ( y e. L -> ( ( `' ( iEdg ` H ) ` y ) = x -> ( ( iEdg ` H ) ` x ) C_ M ) ) )
33 32 rexlimdv 
 |-  ( ( H e. USPGraph /\ x e. dom ( iEdg ` H ) ) -> ( E. y e. L ( `' ( iEdg ` H ) ` y ) = x -> ( ( iEdg ` H ) ` x ) C_ M ) )
34 fveqeq2 
 |-  ( y = ( ( iEdg ` H ) ` x ) -> ( ( `' ( iEdg ` H ) ` y ) = x <-> ( `' ( iEdg ` H ) ` ( ( iEdg ` H ) ` x ) ) = x ) )
35 f1of 
 |-  ( ( iEdg ` H ) : dom ( iEdg ` H ) -1-1-onto-> ( Edg ` H ) -> ( iEdg ` H ) : dom ( iEdg ` H ) --> ( Edg ` H ) )
36 eqid 
 |-  dom ( iEdg ` H ) = dom ( iEdg ` H )
37 2 eqcomi 
 |-  ( Edg ` H ) = J
38 36 37 feq23i 
 |-  ( ( iEdg ` H ) : dom ( iEdg ` H ) --> ( Edg ` H ) <-> ( iEdg ` H ) : dom ( iEdg ` H ) --> J )
39 38 biimpi 
 |-  ( ( iEdg ` H ) : dom ( iEdg ` H ) --> ( Edg ` H ) -> ( iEdg ` H ) : dom ( iEdg ` H ) --> J )
40 5 35 39 3syl 
 |-  ( H e. USPGraph -> ( iEdg ` H ) : dom ( iEdg ` H ) --> J )
41 40 ffvelcdmda 
 |-  ( ( H e. USPGraph /\ x e. dom ( iEdg ` H ) ) -> ( ( iEdg ` H ) ` x ) e. J )
42 41 anim1i 
 |-  ( ( ( H e. USPGraph /\ x e. dom ( iEdg ` H ) ) /\ ( ( iEdg ` H ) ` x ) C_ M ) -> ( ( ( iEdg ` H ) ` x ) e. J /\ ( ( iEdg ` H ) ` x ) C_ M ) )
43 sseq1 
 |-  ( y = ( ( iEdg ` H ) ` x ) -> ( y C_ M <-> ( ( iEdg ` H ) ` x ) C_ M ) )
44 14 43 3 elrab2w 
 |-  ( ( ( iEdg ` H ) ` x ) e. L <-> ( ( ( iEdg ` H ) ` x ) e. J /\ ( ( iEdg ` H ) ` x ) C_ M ) )
45 42 44 sylibr 
 |-  ( ( ( H e. USPGraph /\ x e. dom ( iEdg ` H ) ) /\ ( ( iEdg ` H ) ` x ) C_ M ) -> ( ( iEdg ` H ) ` x ) e. L )
46 f1ocnvfv1 
 |-  ( ( ( iEdg ` H ) : dom ( iEdg ` H ) -1-1-onto-> ( Edg ` H ) /\ x e. dom ( iEdg ` H ) ) -> ( `' ( iEdg ` H ) ` ( ( iEdg ` H ) ` x ) ) = x )
47 5 46 sylan 
 |-  ( ( H e. USPGraph /\ x e. dom ( iEdg ` H ) ) -> ( `' ( iEdg ` H ) ` ( ( iEdg ` H ) ` x ) ) = x )
48 47 adantr 
 |-  ( ( ( H e. USPGraph /\ x e. dom ( iEdg ` H ) ) /\ ( ( iEdg ` H ) ` x ) C_ M ) -> ( `' ( iEdg ` H ) ` ( ( iEdg ` H ) ` x ) ) = x )
49 34 45 48 rspcedvdw 
 |-  ( ( ( H e. USPGraph /\ x e. dom ( iEdg ` H ) ) /\ ( ( iEdg ` H ) ` x ) C_ M ) -> E. y e. L ( `' ( iEdg ` H ) ` y ) = x )
50 49 ex 
 |-  ( ( H e. USPGraph /\ x e. dom ( iEdg ` H ) ) -> ( ( ( iEdg ` H ) ` x ) C_ M -> E. y e. L ( `' ( iEdg ` H ) ` y ) = x ) )
51 33 50 impbid 
 |-  ( ( H e. USPGraph /\ x e. dom ( iEdg ` H ) ) -> ( E. y e. L ( `' ( iEdg ` H ) ` y ) = x <-> ( ( iEdg ` H ) ` x ) C_ M ) )
52 51 rabbidva 
 |-  ( H e. USPGraph -> { x e. dom ( iEdg ` H ) | E. y e. L ( `' ( iEdg ` H ) ` y ) = x } = { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } )
53 13 52 eqtrd 
 |-  ( H e. USPGraph -> ( `' ( iEdg ` H ) " L ) = { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } )