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

Metamath Proof Explorer

Theorem dfgrlic3

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 ‘ 𝐻 )
dfgrlic3.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
dfgrlic3.j ⊢ 𝐽 = ( iEdg ‘ 𝐻 )
dfgrlic3.n ⊢ 𝑁 = ( 𝐺 ClNeighbVtx 𝑣 )
dfgrlic3.m ⊢ 𝑀 = ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) )
dfgrlic3.k ⊢ 𝐾 = { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ 𝑁 }
dfgrlic3.l ⊢ 𝐿 = { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ 𝑀 }
Assertion dfgrlic3 ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ) → ( 𝐺 ≃𝑙𝑔𝑟 𝐻 ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑗 ( 𝑗 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑗 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dfgrlic2.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 dfgrlic2.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
3 dfgrlic3.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
4 dfgrlic3.j ⊢ 𝐽 = ( iEdg ‘ 𝐻 )
5 dfgrlic3.n ⊢ 𝑁 = ( 𝐺 ClNeighbVtx 𝑣 )
6 dfgrlic3.m ⊢ 𝑀 = ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) )
7 dfgrlic3.k ⊢ 𝐾 = { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ 𝑁 }
8 dfgrlic3.l ⊢ 𝐿 = { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ 𝑀 }
9 brgrlic ⊢ ( 𝐺 ≃𝑙𝑔𝑟 𝐻 ↔ ( 𝐺 GraphLocIso 𝐻 ) ≠ ∅ )
10 n0 ⊢ ( ( 𝐺 GraphLocIso 𝐻 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝐺 GraphLocIso 𝐻 ) )
11 9 10 bitri ⊢ ( 𝐺 ≃𝑙𝑔𝑟 𝐻 ↔ ∃ 𝑓 𝑓 ∈ ( 𝐺 GraphLocIso 𝐻 ) )
12 1 2 5 6 3 4 7 8 isgrlim2 ⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝑓 ∈ V ) → ( 𝑓 ∈ ( 𝐺 GraphLocIso 𝐻 ) ↔ ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑗 ( 𝑗 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑗 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) ) )
13 12 el3v3 ⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ) → ( 𝑓 ∈ ( 𝐺 GraphLocIso 𝐻 ) ↔ ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑗 ( 𝑗 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑗 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) ) )
14 13 exbidv ⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ) → ( ∃ 𝑓 𝑓 ∈ ( 𝐺 GraphLocIso 𝐻 ) ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑗 ( 𝑗 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑗 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) ) )
15 11 14 bitrid ⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ) → ( 𝐺 ≃𝑙𝑔𝑟 𝐻 ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑗 ( 𝑗 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑗 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) ) )