Metamath Proof Explorer

Theorem grlimprop

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

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

Proof

Step Hyp Ref Expression
1 grlimprop.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 grlimprop.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
3 grlimdmrel ⊢ Rel dom GraphLocIso
4 3 ovrcl ⊢ ( 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) → ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) )
5 4 simpld ⊢ ( 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) → 𝐺 ∈ V )
6 4 simprd ⊢ ( 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) → 𝐻 ∈ V )
7 id ⊢ ( 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) → 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) )
8 5 6 7 3jca ⊢ ( 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) → ( 𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ) )
9 1 2 isgrlim ⊢ ( ( 𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ) → ( 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) ) ) )
10 9 biimpd ⊢ ( ( 𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ) → ( 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) → ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) ) ) )
11 8 10 mpcom ⊢ ( 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) → ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) ) )