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

Metamath Proof Explorer

Theorem usgrlimprop

Description: Properties of a local isomorphism of simple pseudographs. (Contributed by AV, 17-Aug-2025)

Ref Expression
Hypotheses usgrlimprop.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
usgrlimprop.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
usgrlimprop.n ⊢ 𝑁 = ( 𝐺 ClNeighbVtx 𝑣 )
usgrlimprop.m ⊢ 𝑀 = ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) )
usgrlimprop.i ⊢ 𝐼 = ( Edg ‘ 𝐺 )
usgrlimprop.j ⊢ 𝐽 = ( Edg ‘ 𝐻 )
usgrlimprop.k ⊢ 𝐾 = { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁 }
usgrlimprop.l ⊢ 𝐿 = { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀 }
Assertion usgrlimprop ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ) → ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 usgrlimprop.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 usgrlimprop.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
3 usgrlimprop.n ⊢ 𝑁 = ( 𝐺 ClNeighbVtx 𝑣 )
4 usgrlimprop.m ⊢ 𝑀 = ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) )
5 usgrlimprop.i ⊢ 𝐼 = ( Edg ‘ 𝐺 )
6 usgrlimprop.j ⊢ 𝐽 = ( Edg ‘ 𝐻 )
7 usgrlimprop.k ⊢ 𝐾 = { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁 }
8 usgrlimprop.l ⊢ 𝐿 = { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀 }
9 simp3 ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ) → 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) )
10 1 2 3 4 5 6 7 8 uspgrlim ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ) → ( 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) ) )
11 9 10 mpbid ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ) → ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) )