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

Metamath Proof Explorer

Theorem uhgrimgrlim

Description: An isomorphism of hypergraphs is a local isomorphism between the two graphs. (Contributed by AV, 2-Jun-2025)

Ref Expression
Assertion uhgrimgrlim ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 eqid ⊢ ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐻 )
3 1 2 grimf1o ⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) )
4 3 3ad2ant3 ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) )
5 simpl1 ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ∧ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → 𝐺 ∈ UHGraph )
6 simpl3 ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ∧ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) )
7 1 clnbgrssvtx ⊢ ( 𝐺 ClNeighbVtx 𝑣 ) ⊆ ( Vtx ‘ 𝐺 )
8 7 a1i ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ∧ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 ClNeighbVtx 𝑣 ) ⊆ ( Vtx ‘ 𝐺 ) )
9 1 uhgrimisgrgric ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝐺 ClNeighbVtx 𝑣 ) ⊆ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐹 “ ( 𝐺 ClNeighbVtx 𝑣 ) ) ) )
10 5 6 8 9 syl3anc ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ∧ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐹 “ ( 𝐺 ClNeighbVtx 𝑣 ) ) ) )
11 df-3an ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ↔ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) )
12 1 clnbgrgrim ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ∧ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) = ( 𝐹 “ ( 𝐺 ClNeighbVtx 𝑣 ) ) )
13 11 12 sylanb ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ∧ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) = ( 𝐹 “ ( 𝐺 ClNeighbVtx 𝑣 ) ) )
14 13 oveq2d ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ∧ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) = ( 𝐻 ISubGr ( 𝐹 “ ( 𝐺 ClNeighbVtx 𝑣 ) ) ) )
15 10 14 breqtrrd ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ∧ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) )
16 15 ralrimiva ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) )
17 1 2 isgrlim ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ↔ ( 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) ) ) )
18 4 16 17 mpbir2and ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) )