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

Metamath Proof Explorer

Theorem dfgrlic2

Description: Alternate, explicit definition of the "is locally isomorphic to" relation for two graphs. (Contributed by AV, 9-Jun-2025)

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

Proof

Step Hyp Ref Expression
1 dfgrlic2.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 dfgrlic2.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
3 brgrlic ⊢ ( 𝐺 ≃𝑙𝑔𝑟 𝐻 ↔ ( 𝐺 GraphLocIso 𝐻 ) ≠ ∅ )
4 n0 ⊢ ( ( 𝐺 GraphLocIso 𝐻 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝐺 GraphLocIso 𝐻 ) )
5 3 4 bitri ⊢ ( 𝐺 ≃𝑙𝑔𝑟 𝐻 ↔ ∃ 𝑓 𝑓 ∈ ( 𝐺 GraphLocIso 𝐻 ) )
6 1 2 isgrlim ⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝑓 ∈ V ) → ( 𝑓 ∈ ( 𝐺 GraphLocIso 𝐻 ) ↔ ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) ) )
7 6 el3v3 ⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ) → ( 𝑓 ∈ ( 𝐺 GraphLocIso 𝐻 ) ↔ ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) ) )
8 7 exbidv ⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ) → ( ∃ 𝑓 𝑓 ∈ ( 𝐺 GraphLocIso 𝐻 ) ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) ) )
9 5 8 bitrid ⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ) → ( 𝐺 ≃𝑙𝑔𝑟 𝐻 ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) ) )