Metamath Proof Explorer

Theorem grlimgredgex

Description: Local isomorphisms between simple pseudographs map an edge onto an edge with an endpoint being the image of one of the endpoints of the first edge under the local isomorphism. (Contributed by AV, 28-Dec-2025)

Ref Expression
Hypotheses grlimgredgex.i 
|- I = ( Edg ` G )
grlimgredgex.e 
|- E = ( Edg ` H )
grlimgredgex.v 
|- V = ( Vtx ` H )
grlimgredgex.a 
|- ( ph -> A e. X )
grlimgredgex.b 
|- ( ph -> B e. Y )
grlimgredgex.p 
|- ( ph -> { A , B } e. I )
grlimgredgex.g 
|- ( ph -> G e. USPGraph )
grlimgredgex.h 
|- ( ph -> H e. USPGraph )
grlimgredgex.f 
|- ( ph -> F e. ( G GraphLocIso H ) )
Assertion grlimgredgex 
|- ( ph -> E. v e. V { ( F ` A ) , v } e. E )

Proof

Step Hyp Ref Expression
1 grlimgredgex.i 
 |-  I = ( Edg ` G )
2 grlimgredgex.e 
 |-  E = ( Edg ` H )
3 grlimgredgex.v 
 |-  V = ( Vtx ` H )
4 grlimgredgex.a 
 |-  ( ph -> A e. X )
5 grlimgredgex.b 
 |-  ( ph -> B e. Y )
6 grlimgredgex.p 
 |-  ( ph -> { A , B } e. I )
7 grlimgredgex.g 
 |-  ( ph -> G e. USPGraph )
8 grlimgredgex.h 
 |-  ( ph -> H e. USPGraph )
9 grlimgredgex.f 
 |-  ( ph -> F e. ( G GraphLocIso H ) )
10 eqid 
 |-  ( G ClNeighbVtx A ) = ( G ClNeighbVtx A )
11 eqid 
 |-  { x e. I | x C_ ( G ClNeighbVtx A ) } = { x e. I | x C_ ( G ClNeighbVtx A ) }
12 eqid 
 |-  ( H ClNeighbVtx ( F ` A ) ) = ( H ClNeighbVtx ( F ` A ) )
13 eqid 
 |-  { x e. E | x C_ ( H ClNeighbVtx ( F ` A ) ) } = { x e. E | x C_ ( H ClNeighbVtx ( F ` A ) ) }
14 10 1 11 12 2 13 grlimprclnbgrvtx 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. X /\ B e. Y /\ { A , B } e. I ) ) -> E. f ( f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) /\ ( { ( F ` A ) , ( f ` B ) } e. { x e. E | x C_ ( H ClNeighbVtx ( F ` A ) ) } \/ { ( F ` A ) , ( f ` A ) } e. { x e. E | x C_ ( H ClNeighbVtx ( F ` A ) ) } ) ) )
15 7 8 9 4 5 6 14 syl213anc 
 |-  ( ph -> E. f ( f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) /\ ( { ( F ` A ) , ( f ` B ) } e. { x e. E | x C_ ( H ClNeighbVtx ( F ` A ) ) } \/ { ( F ` A ) , ( f ` A ) } e. { x e. E | x C_ ( H ClNeighbVtx ( F ` A ) ) } ) ) )
16 f1of 
 |-  ( f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) -> f : ( G ClNeighbVtx A ) --> ( H ClNeighbVtx ( F ` A ) ) )
17 16 adantl 
 |-  ( ( ph /\ f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) ) -> f : ( G ClNeighbVtx A ) --> ( H ClNeighbVtx ( F ` A ) ) )
18 uspgrupgr 
 |-  ( G e. USPGraph -> G e. UPGraph )
19 7 18 syl 
 |-  ( ph -> G e. UPGraph )
20 4 5 jca 
 |-  ( ph -> ( A e. X /\ B e. Y ) )
21 19 20 6 3jca 
 |-  ( ph -> ( G e. UPGraph /\ ( A e. X /\ B e. Y ) /\ { A , B } e. I ) )
22 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
23 22 1 upgrpredgv 
 |-  ( ( G e. UPGraph /\ ( A e. X /\ B e. Y ) /\ { A , B } e. I ) -> ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) )
24 simpr 
 |-  ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) -> B e. ( Vtx ` G ) )
25 21 23 24 3syl 
 |-  ( ph -> B e. ( Vtx ` G ) )
26 simpl 
 |-  ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) -> A e. ( Vtx ` G ) )
27 21 23 26 3syl 
 |-  ( ph -> A e. ( Vtx ` G ) )
28 22 1 predgclnbgrel 
 |-  ( ( B e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) /\ { A , B } e. I ) -> B e. ( G ClNeighbVtx A ) )
29 25 27 6 28 syl3anc 
 |-  ( ph -> B e. ( G ClNeighbVtx A ) )
30 29 adantr 
 |-  ( ( ph /\ f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) ) -> B e. ( G ClNeighbVtx A ) )
31 17 30 ffvelcdmd 
 |-  ( ( ph /\ f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) ) -> ( f ` B ) e. ( H ClNeighbVtx ( F ` A ) ) )
32 3 clnbgrisvtx 
 |-  ( ( f ` B ) e. ( H ClNeighbVtx ( F ` A ) ) -> ( f ` B ) e. V )
33 31 32 syl 
 |-  ( ( ph /\ f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) ) -> ( f ` B ) e. V )
34 33 adantr 
 |-  ( ( ( ph /\ f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) ) /\ { ( F ` A ) , ( f ` B ) } e. { x e. E | x C_ ( H ClNeighbVtx ( F ` A ) ) } ) -> ( f ` B ) e. V )
35 preq2 
 |-  ( v = ( f ` B ) -> { ( F ` A ) , v } = { ( F ` A ) , ( f ` B ) } )
36 35 eleq1d 
 |-  ( v = ( f ` B ) -> ( { ( F ` A ) , v } e. E <-> { ( F ` A ) , ( f ` B ) } e. E ) )
37 36 adantl 
 |-  ( ( ( ( ph /\ f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) ) /\ { ( F ` A ) , ( f ` B ) } e. { x e. E | x C_ ( H ClNeighbVtx ( F ` A ) ) } ) /\ v = ( f ` B ) ) -> ( { ( F ` A ) , v } e. E <-> { ( F ` A ) , ( f ` B ) } e. E ) )
38 sseq1 
 |-  ( x = { ( F ` A ) , ( f ` B ) } -> ( x C_ ( H ClNeighbVtx ( F ` A ) ) <-> { ( F ` A ) , ( f ` B ) } C_ ( H ClNeighbVtx ( F ` A ) ) ) )
39 38 elrab 
 |-  ( { ( F ` A ) , ( f ` B ) } e. { x e. E | x C_ ( H ClNeighbVtx ( F ` A ) ) } <-> ( { ( F ` A ) , ( f ` B ) } e. E /\ { ( F ` A ) , ( f ` B ) } C_ ( H ClNeighbVtx ( F ` A ) ) ) )
40 39 simplbi 
 |-  ( { ( F ` A ) , ( f ` B ) } e. { x e. E | x C_ ( H ClNeighbVtx ( F ` A ) ) } -> { ( F ` A ) , ( f ` B ) } e. E )
41 40 adantl 
 |-  ( ( ( ph /\ f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) ) /\ { ( F ` A ) , ( f ` B ) } e. { x e. E | x C_ ( H ClNeighbVtx ( F ` A ) ) } ) -> { ( F ` A ) , ( f ` B ) } e. E )
42 34 37 41 rspcedvd 
 |-  ( ( ( ph /\ f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) ) /\ { ( F ` A ) , ( f ` B ) } e. { x e. E | x C_ ( H ClNeighbVtx ( F ` A ) ) } ) -> E. v e. V { ( F ` A ) , v } e. E )
43 42 ex 
 |-  ( ( ph /\ f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) ) -> ( { ( F ` A ) , ( f ` B ) } e. { x e. E | x C_ ( H ClNeighbVtx ( F ` A ) ) } -> E. v e. V { ( F ` A ) , v } e. E ) )
44 22 clnbgrvtxel 
 |-  ( A e. ( Vtx ` G ) -> A e. ( G ClNeighbVtx A ) )
45 27 44 syl 
 |-  ( ph -> A e. ( G ClNeighbVtx A ) )
46 45 adantr 
 |-  ( ( ph /\ f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) ) -> A e. ( G ClNeighbVtx A ) )
47 17 46 ffvelcdmd 
 |-  ( ( ph /\ f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) ) -> ( f ` A ) e. ( H ClNeighbVtx ( F ` A ) ) )
48 3 clnbgrisvtx 
 |-  ( ( f ` A ) e. ( H ClNeighbVtx ( F ` A ) ) -> ( f ` A ) e. V )
49 47 48 syl 
 |-  ( ( ph /\ f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) ) -> ( f ` A ) e. V )
50 49 adantr 
 |-  ( ( ( ph /\ f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) ) /\ { ( F ` A ) , ( f ` A ) } e. { x e. E | x C_ ( H ClNeighbVtx ( F ` A ) ) } ) -> ( f ` A ) e. V )
51 preq2 
 |-  ( v = ( f ` A ) -> { ( F ` A ) , v } = { ( F ` A ) , ( f ` A ) } )
52 51 eleq1d 
 |-  ( v = ( f ` A ) -> ( { ( F ` A ) , v } e. E <-> { ( F ` A ) , ( f ` A ) } e. E ) )
53 52 adantl 
 |-  ( ( ( ( ph /\ f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) ) /\ { ( F ` A ) , ( f ` A ) } e. { x e. E | x C_ ( H ClNeighbVtx ( F ` A ) ) } ) /\ v = ( f ` A ) ) -> ( { ( F ` A ) , v } e. E <-> { ( F ` A ) , ( f ` A ) } e. E ) )
54 sseq1 
 |-  ( x = { ( F ` A ) , ( f ` A ) } -> ( x C_ ( H ClNeighbVtx ( F ` A ) ) <-> { ( F ` A ) , ( f ` A ) } C_ ( H ClNeighbVtx ( F ` A ) ) ) )
55 54 elrab 
 |-  ( { ( F ` A ) , ( f ` A ) } e. { x e. E | x C_ ( H ClNeighbVtx ( F ` A ) ) } <-> ( { ( F ` A ) , ( f ` A ) } e. E /\ { ( F ` A ) , ( f ` A ) } C_ ( H ClNeighbVtx ( F ` A ) ) ) )
56 55 simplbi 
 |-  ( { ( F ` A ) , ( f ` A ) } e. { x e. E | x C_ ( H ClNeighbVtx ( F ` A ) ) } -> { ( F ` A ) , ( f ` A ) } e. E )
57 56 adantl 
 |-  ( ( ( ph /\ f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) ) /\ { ( F ` A ) , ( f ` A ) } e. { x e. E | x C_ ( H ClNeighbVtx ( F ` A ) ) } ) -> { ( F ` A ) , ( f ` A ) } e. E )
58 50 53 57 rspcedvd 
 |-  ( ( ( ph /\ f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) ) /\ { ( F ` A ) , ( f ` A ) } e. { x e. E | x C_ ( H ClNeighbVtx ( F ` A ) ) } ) -> E. v e. V { ( F ` A ) , v } e. E )
59 58 ex 
 |-  ( ( ph /\ f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) ) -> ( { ( F ` A ) , ( f ` A ) } e. { x e. E | x C_ ( H ClNeighbVtx ( F ` A ) ) } -> E. v e. V { ( F ` A ) , v } e. E ) )
60 43 59 jaod 
 |-  ( ( ph /\ f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) ) -> ( ( { ( F ` A ) , ( f ` B ) } e. { x e. E | x C_ ( H ClNeighbVtx ( F ` A ) ) } \/ { ( F ` A ) , ( f ` A ) } e. { x e. E | x C_ ( H ClNeighbVtx ( F ` A ) ) } ) -> E. v e. V { ( F ` A ) , v } e. E ) )
61 60 expimpd 
 |-  ( ph -> ( ( f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) /\ ( { ( F ` A ) , ( f ` B ) } e. { x e. E | x C_ ( H ClNeighbVtx ( F ` A ) ) } \/ { ( F ` A ) , ( f ` A ) } e. { x e. E | x C_ ( H ClNeighbVtx ( F ` A ) ) } ) ) -> E. v e. V { ( F ` A ) , v } e. E ) )
62 61 exlimdv 
 |-  ( ph -> ( E. f ( f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) /\ ( { ( F ` A ) , ( f ` B ) } e. { x e. E | x C_ ( H ClNeighbVtx ( F ` A ) ) } \/ { ( F ` A ) , ( f ` A ) } e. { x e. E | x C_ ( H ClNeighbVtx ( F ` A ) ) } ) ) -> E. v e. V { ( F ` A ) , v } e. E ) )
63 15 62 mpd 
 |-  ( ph -> E. v e. V { ( F ` A ) , v } e. E )