Theorem dfgrlic2

Description: Alternate, explicit definition of the "is locally isomorphic to" relation for two graphs. (Contributed by AV, 9-Jun-2025)

	Ref	Expression
Hypotheses	dfgrlic2.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	dfgrlic2.w	⊢ 𝑊 = ( Vtx ‘ 𝐻 )
Assertion	dfgrlic2	⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ) → ( 𝐺 ≃𝑙𝑔𝑟 𝐻 ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfgrlic2.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		dfgrlic2.w	⊢ 𝑊 = ( Vtx ‘ 𝐻 )
3		brgrlic	⊢ ( 𝐺 ≃𝑙𝑔𝑟 𝐻 ↔ ( 𝐺 GraphLocIso 𝐻 ) ≠ ∅ )
4		n0	⊢ ( ( 𝐺 GraphLocIso 𝐻 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝐺 GraphLocIso 𝐻 ) )
5	3 4	bitri	⊢ ( 𝐺 ≃𝑙𝑔𝑟 𝐻 ↔ ∃ 𝑓 𝑓 ∈ ( 𝐺 GraphLocIso 𝐻 ) )
6	1 2	isgrlim	⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝑓 ∈ V ) → ( 𝑓 ∈ ( 𝐺 GraphLocIso 𝐻 ) ↔ ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) ) )
7	6	el3v3	⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ) → ( 𝑓 ∈ ( 𝐺 GraphLocIso 𝐻 ) ↔ ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) ) )
8	7	exbidv	⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ) → ( ∃ 𝑓 𝑓 ∈ ( 𝐺 GraphLocIso 𝐻 ) ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) ) )
9	5 8	bitrid	⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ) → ( 𝐺 ≃𝑙𝑔𝑟 𝐻 ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) ) )