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

Metamath Proof Explorer

Theorem grlimprop2

Description: Properties of a local isomorphism of graphs. (Contributed by AV, 29-May-2025)

Ref Expression
Hypotheses grlimprop.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
grlimprop.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
grlimprop2.n ⊢ 𝑁 = ( 𝐺 ClNeighbVtx 𝑣 )
grlimprop2.m ⊢ 𝑀 = ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) )
grlimprop2.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
grlimprop2.j ⊢ 𝐽 = ( iEdg ‘ 𝐻 )
grlimprop2.k ⊢ 𝐾 = { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ 𝑁 }
grlimprop2.l ⊢ 𝐿 = { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ 𝑀 }
Assertion grlimprop2 ( 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) → ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 grlimprop.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 grlimprop.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
3 grlimprop2.n ⊢ 𝑁 = ( 𝐺 ClNeighbVtx 𝑣 )
4 grlimprop2.m ⊢ 𝑀 = ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) )
5 grlimprop2.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
6 grlimprop2.j ⊢ 𝐽 = ( iEdg ‘ 𝐻 )
7 grlimprop2.k ⊢ 𝐾 = { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ 𝑁 }
8 grlimprop2.l ⊢ 𝐿 = { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ 𝑀 }
9 grlimdmrel ⊢ Rel dom GraphLocIso
10 9 ovrcl ⊢ ( 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) → ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) )
11 id ⊢ ( 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) → 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) )
12 df-3an ⊢ ( ( 𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ) ↔ ( ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ) )
13 10 11 12 sylanbrc ⊢ ( 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) → ( 𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ) )
14 1 2 3 4 5 6 7 8 isgrlim2 ⊢ ( ( 𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ) → ( 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) ) )
15 13 14 syl ⊢ ( 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) → ( 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) ) )
16 15 ibi ⊢ ( 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) → ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )