Theorem grilcbri

Description: Implications of two graphs being locally isomorphic. (Contributed by AV, 9-Jun-2025)

	Ref	Expression
Hypotheses	dfgrlic2.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	dfgrlic2.w	⊢ 𝑊 = ( Vtx ‘ 𝐻 )
Assertion	grilcbri	⊢ ( 𝐺 ≃𝑙𝑔𝑟 𝐻 → ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfgrlic2.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		dfgrlic2.w	⊢ 𝑊 = ( Vtx ‘ 𝐻 )
3		grlicrcl	⊢ ( 𝐺 ≃𝑙𝑔𝑟 𝐻 → ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) )
4	1 2	dfgrlic2	⊢ ( ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) → ( 𝐺 ≃𝑙𝑔𝑟 𝐻 ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) ) )
5	3 4	syl	⊢ ( 𝐺 ≃𝑙𝑔𝑟 𝐻 → ( 𝐺 ≃𝑙𝑔𝑟 𝐻 ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) ) )
6	5	ibi	⊢ ( 𝐺 ≃𝑙𝑔𝑟 𝐻 → ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) )