Metamath Proof Explorer

Theorem uspgrlimlem1

Description: Lemma 1 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 uspgrlimlem1 
|- ( H e. USPGraph -> L = ( ( iEdg ` H ) " { 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 f1of 
 |-  ( ( iEdg ` H ) : dom ( iEdg ` H ) -1-1-onto-> ( Edg ` H ) -> ( iEdg ` H ) : dom ( iEdg ` H ) --> ( Edg ` H ) )
7 5 6 syl 
 |-  ( H e. USPGraph -> ( iEdg ` H ) : dom ( iEdg ` H ) --> ( Edg ` H ) )
8 ssrab2 
 |-  { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } C_ dom ( iEdg ` H )
9 fimarab 
 |-  ( ( ( iEdg ` H ) : dom ( iEdg ` H ) --> ( Edg ` H ) /\ { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } C_ dom ( iEdg ` H ) ) -> ( ( iEdg ` H ) " { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } ) = { y e. ( Edg ` H ) | E. z e. { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } ( ( iEdg ` H ) ` z ) = y } )
10 7 8 9 sylancl 
 |-  ( H e. USPGraph -> ( ( iEdg ` H ) " { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } ) = { y e. ( Edg ` H ) | E. z e. { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } ( ( iEdg ` H ) ` z ) = y } )
11 2 eqcomi 
 |-  ( Edg ` H ) = J
12 11 a1i 
 |-  ( H e. USPGraph -> ( Edg ` H ) = J )
13 fveq2 
 |-  ( x = z -> ( ( iEdg ` H ) ` x ) = ( ( iEdg ` H ) ` z ) )
14 13 sseq1d 
 |-  ( x = z -> ( ( ( iEdg ` H ) ` x ) C_ M <-> ( ( iEdg ` H ) ` z ) C_ M ) )
15 14 rexrab 
 |-  ( E. z e. { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } ( ( iEdg ` H ) ` z ) = y <-> E. z e. dom ( iEdg ` H ) ( ( ( iEdg ` H ) ` z ) C_ M /\ ( ( iEdg ` H ) ` z ) = y ) )
16 sseq1 
 |-  ( ( ( iEdg ` H ) ` z ) = y -> ( ( ( iEdg ` H ) ` z ) C_ M <-> y C_ M ) )
17 16 biimpac 
 |-  ( ( ( ( iEdg ` H ) ` z ) C_ M /\ ( ( iEdg ` H ) ` z ) = y ) -> y C_ M )
18 17 a1i 
 |-  ( ( ( H e. USPGraph /\ y e. ( Edg ` H ) ) /\ z e. dom ( iEdg ` H ) ) -> ( ( ( ( iEdg ` H ) ` z ) C_ M /\ ( ( iEdg ` H ) ` z ) = y ) -> y C_ M ) )
19 f1ocnv 
 |-  ( ( iEdg ` H ) : dom ( iEdg ` H ) -1-1-onto-> ( Edg ` H ) -> `' ( iEdg ` H ) : ( Edg ` H ) -1-1-onto-> dom ( iEdg ` H ) )
20 f1of 
 |-  ( `' ( iEdg ` H ) : ( Edg ` H ) -1-1-onto-> dom ( iEdg ` H ) -> `' ( iEdg ` H ) : ( Edg ` H ) --> dom ( iEdg ` H ) )
21 5 19 20 3syl 
 |-  ( H e. USPGraph -> `' ( iEdg ` H ) : ( Edg ` H ) --> dom ( iEdg ` H ) )
22 21 ffvelcdmda 
 |-  ( ( H e. USPGraph /\ y e. ( Edg ` H ) ) -> ( `' ( iEdg ` H ) ` y ) e. dom ( iEdg ` H ) )
23 22 adantr 
 |-  ( ( ( H e. USPGraph /\ y e. ( Edg ` H ) ) /\ y C_ M ) -> ( `' ( iEdg ` H ) ` y ) e. dom ( iEdg ` H ) )
24 f1ocnvfv2 
 |-  ( ( ( iEdg ` H ) : dom ( iEdg ` H ) -1-1-onto-> ( Edg ` H ) /\ y e. ( Edg ` H ) ) -> ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) = y )
25 5 24 sylan 
 |-  ( ( H e. USPGraph /\ y e. ( Edg ` H ) ) -> ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) = y )
26 25 adantr 
 |-  ( ( ( H e. USPGraph /\ y e. ( Edg ` H ) ) /\ y C_ M ) -> ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) = y )
27 sseq1 
 |-  ( y = ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) -> ( y C_ M <-> ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) C_ M ) )
28 27 eqcoms 
 |-  ( ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) = y -> ( y C_ M <-> ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) C_ M ) )
29 28 biimpcd 
 |-  ( y C_ M -> ( ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) = y -> ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) C_ M ) )
30 29 adantl 
 |-  ( ( ( H e. USPGraph /\ y e. ( Edg ` H ) ) /\ y C_ M ) -> ( ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) = y -> ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) C_ M ) )
31 30 ancrd 
 |-  ( ( ( H e. USPGraph /\ y e. ( Edg ` H ) ) /\ y C_ M ) -> ( ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) = y -> ( ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) C_ M /\ ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) = y ) ) )
32 26 31 mpd 
 |-  ( ( ( H e. USPGraph /\ y e. ( Edg ` H ) ) /\ y C_ M ) -> ( ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) C_ M /\ ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) = y ) )
33 fveq2 
 |-  ( z = ( `' ( iEdg ` H ) ` y ) -> ( ( iEdg ` H ) ` z ) = ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) )
34 33 sseq1d 
 |-  ( z = ( `' ( iEdg ` H ) ` y ) -> ( ( ( iEdg ` H ) ` z ) C_ M <-> ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) C_ M ) )
35 fveqeq2 
 |-  ( z = ( `' ( iEdg ` H ) ` y ) -> ( ( ( iEdg ` H ) ` z ) = y <-> ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) = y ) )
36 34 35 anbi12d 
 |-  ( z = ( `' ( iEdg ` H ) ` y ) -> ( ( ( ( iEdg ` H ) ` z ) C_ M /\ ( ( iEdg ` H ) ` z ) = y ) <-> ( ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) C_ M /\ ( ( iEdg ` H ) ` ( `' ( iEdg ` H ) ` y ) ) = y ) ) )
37 18 23 32 36 rspceb2dv 
 |-  ( ( H e. USPGraph /\ y e. ( Edg ` H ) ) -> ( E. z e. dom ( iEdg ` H ) ( ( ( iEdg ` H ) ` z ) C_ M /\ ( ( iEdg ` H ) ` z ) = y ) <-> y C_ M ) )
38 15 37 bitrid 
 |-  ( ( H e. USPGraph /\ y e. ( Edg ` H ) ) -> ( E. z e. { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } ( ( iEdg ` H ) ` z ) = y <-> y C_ M ) )
39 12 38 rabeqbidva 
 |-  ( H e. USPGraph -> { y e. ( Edg ` H ) | E. z e. { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } ( ( iEdg ` H ) ` z ) = y } = { y e. J | y C_ M } )
40 sseq1 
 |-  ( y = x -> ( y C_ M <-> x C_ M ) )
41 40 cbvrabv 
 |-  { y e. J | y C_ M } = { x e. J | x C_ M }
42 41 a1i 
 |-  ( H e. USPGraph -> { y e. J | y C_ M } = { x e. J | x C_ M } )
43 10 39 42 3eqtrrd 
 |-  ( H e. USPGraph -> { x e. J | x C_ M } = ( ( iEdg ` H ) " { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } ) )
44 3 43 eqtrid 
 |-  ( H e. USPGraph -> L = ( ( iEdg ` H ) " { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } ) )