isgrlim2

Description: A local isomorphism of graphs is a bijection between their vertices that preserves neighborhoods. Definitions expanded. (Contributed by AV, 29-May-2025)

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

Proof

Step	Hyp	Ref	Expression
1		isgrlim.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		isgrlim.w	⊢ 𝑊 = ( Vtx ‘ 𝐻 )
3		isgrlim2.n	⊢ 𝑁 = ( 𝐺 ClNeighbVtx 𝑣 )
4		isgrlim2.m	⊢ 𝑀 = ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) )
5		isgrlim2.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
6		isgrlim2.j	⊢ 𝐽 = ( iEdg ‘ 𝐻 )
7		isgrlim2.k	⊢ 𝐾 = { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ 𝑁 }
8		isgrlim2.l	⊢ 𝐿 = { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ 𝑀 }
9	1 2	isgrlim	⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍 ) → ( 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃_𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) ) ) )
10	3	eqcomi	⊢ ( 𝐺 ClNeighbVtx 𝑣 ) = 𝑁
11	10	oveq2i	⊢ ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) = ( 𝐺 ISubGr 𝑁 )
12	4	eqcomi	⊢ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) = 𝑀
13	12	oveq2i	⊢ ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) = ( 𝐻 ISubGr 𝑀 )
14	11 13	breq12i	⊢ ( ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃_𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) ↔ ( 𝐺 ISubGr 𝑁 ) ≃_𝑔𝑟 ( 𝐻 ISubGr 𝑀 ) )
15	14	a1i	⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍 ) → ( ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃_𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) ↔ ( 𝐺 ISubGr 𝑁 ) ≃_𝑔𝑟 ( 𝐻 ISubGr 𝑀 ) ) )
16	5 6 3 4 7 8	clnbgrisubgrgrim	⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ) → ( ( 𝐺 ISubGr 𝑁 ) ≃_𝑔𝑟 ( 𝐻 ISubGr 𝑀 ) ↔ ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )
17	16	3adant3	⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍 ) → ( ( 𝐺 ISubGr 𝑁 ) ≃_𝑔𝑟 ( 𝐻 ISubGr 𝑀 ) ↔ ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )
18	15 17	bitrd	⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍 ) → ( ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃_𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) ↔ ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )
19	18	ralbidv	⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍 ) → ( ∀ 𝑣 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃_𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) ↔ ∀ 𝑣 ∈ 𝑉 ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )
20	19	anbi2d	⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍 ) → ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃_𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) ) ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) ) )
21	9 20	bitrd	⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍 ) → ( 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) ) )

Metamath Proof Explorer

Theorem isgrlim2

Proof