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

Metamath Proof Explorer

Theorem clnbgrisubgrgrim

Description: Isomorphic subgraphs induced by closed neighborhoods of vertices of two graphs. (Contributed by AV, 29-May-2025)

Ref Expression
Hypotheses clnbgrisubgrgrim.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
clnbgrisubgrgrim.j ⊢ 𝐽 = ( iEdg ‘ 𝐻 )
clnbgrisubgrgrim.n ⊢ 𝑁 = ( 𝐺 ClNeighbVtx 𝑋 )
clnbgrisubgrgrim.m ⊢ 𝑀 = ( 𝐻 ClNeighbVtx 𝑌 )
clnbgrisubgrgrim.k ⊢ 𝐾 = { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ 𝑁 }
clnbgrisubgrgrim.l ⊢ 𝐿 = { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ 𝑀 }
Assertion clnbgrisubgrgrim ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) → ( ( 𝐺 ISubGr 𝑁 ) ≃𝑔𝑟 ( 𝐻 ISubGr 𝑀 ) ↔ ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 clnbgrisubgrgrim.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2 clnbgrisubgrgrim.j ⊢ 𝐽 = ( iEdg ‘ 𝐻 )
3 clnbgrisubgrgrim.n ⊢ 𝑁 = ( 𝐺 ClNeighbVtx 𝑋 )
4 clnbgrisubgrgrim.m ⊢ 𝑀 = ( 𝐻 ClNeighbVtx 𝑌 )
5 clnbgrisubgrgrim.k ⊢ 𝐾 = { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ 𝑁 }
6 clnbgrisubgrgrim.l ⊢ 𝐿 = { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ 𝑀 }
7 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
8 7 clnbgrssvtx ⊢ ( 𝐺 ClNeighbVtx 𝑋 ) ⊆ ( Vtx ‘ 𝐺 )
9 3 8 eqsstri ⊢ 𝑁 ⊆ ( Vtx ‘ 𝐺 )
10 eqid ⊢ ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐻 )
11 10 clnbgrssvtx ⊢ ( 𝐻 ClNeighbVtx 𝑌 ) ⊆ ( Vtx ‘ 𝐻 )
12 4 11 eqsstri ⊢ 𝑀 ⊆ ( Vtx ‘ 𝐻 )
13 7 10 1 2 5 6 isubgrgrim ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ ( Vtx ‘ 𝐺 ) ∧ 𝑀 ⊆ ( Vtx ‘ 𝐻 ) ) ) → ( ( 𝐺 ISubGr 𝑁 ) ≃𝑔𝑟 ( 𝐻 ISubGr 𝑀 ) ↔ ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )
14 9 12 13 mpanr12 ⊢ ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) → ( ( 𝐺 ISubGr 𝑁 ) ≃𝑔𝑟 ( 𝐻 ISubGr 𝑀 ) ↔ ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )