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→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )