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

Metamath Proof Explorer

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 ( 𝑓 ‘ 𝑣 ) ) ) ) )