This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grlimpredg

Description: For two locally isomorphic graphs G and H and a vertex A of G there is a bijection f mapping the closed neighborhood N of A onto the closed neighborhood M of ( FA ) , so that the mapped vertices of an edge { A , B } containing the vertex A is an edge in H . (Contributed by AV, 27-Dec-2025)

Ref Expression
Hypotheses clnbgrvtxedg.n ⊢ 𝑁 = ( 𝐺 ClNeighbVtx 𝐴 )
clnbgrvtxedg.i ⊢ 𝐼 = ( Edg ‘ 𝐺 )
clnbgrvtxedg.k ⊢ 𝐾 = { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁 }
grlimedgclnbgr.m ⊢ 𝑀 = ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) )
grlimedgclnbgr.j ⊢ 𝐽 = ( Edg ‘ 𝐻 )
grlimedgclnbgr.l ⊢ 𝐿 = { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀 }
Assertion grlimpredg ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 clnbgrvtxedg.n ⊢ 𝑁 = ( 𝐺 ClNeighbVtx 𝐴 )
2 clnbgrvtxedg.i ⊢ 𝐼 = ( Edg ‘ 𝐺 )
3 clnbgrvtxedg.k ⊢ 𝐾 = { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁 }
4 grlimedgclnbgr.m ⊢ 𝑀 = ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) )
5 grlimedgclnbgr.j ⊢ 𝐽 = ( Edg ‘ 𝐻 )
6 grlimedgclnbgr.l ⊢ 𝐿 = { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀 }
7 1 2 3 4 5 6 grlimprclnbgredg ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) )
8 sseq1 ⊢ ( 𝑥 = { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } → ( 𝑥 ⊆ 𝑀 ↔ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ⊆ 𝑀 ) )
9 8 6 elrab2 ⊢ ( { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ↔ ( { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ⊆ 𝑀 ) )
10 simpl ⊢ ( ( { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ⊆ 𝑀 ) → { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 )
11 10 a1i ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) → ( ( { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ⊆ 𝑀 ) → { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ) )
12 9 11 biimtrid ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) → ( { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 → { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ) )
13 12 imdistanda ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → ( ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) → ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ) ) )
14 13 eximdv ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → ( ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) → ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ) ) )
15 7 14 mpd ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ) )