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→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ) )