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

Metamath Proof Explorer

Theorem uhgrspan1lem3

Description: Lemma 3 for uhgrspan1 . (Contributed by AV, 19-Nov-2020)

Ref Expression
Hypotheses uhgrspan1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
uhgrspan1.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
uhgrspan1.f ⊢ 𝐹 = { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∉ ( 𝐼 ‘ 𝑖 ) }
uhgrspan1.s ⊢ 𝑆 = ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( 𝐼 ↾ 𝐹 ) ⟩
Assertion uhgrspan1lem3 ( iEdg ‘ 𝑆 ) = ( 𝐼 ↾ 𝐹 )

Proof

Step Hyp Ref Expression
1 uhgrspan1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 uhgrspan1.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 uhgrspan1.f ⊢ 𝐹 = { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∉ ( 𝐼 ‘ 𝑖 ) }
4 uhgrspan1.s ⊢ 𝑆 = ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( 𝐼 ↾ 𝐹 ) ⟩
5 4 fveq2i ⊢ ( iEdg ‘ 𝑆 ) = ( iEdg ‘ ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( 𝐼 ↾ 𝐹 ) ⟩ )
6 1 2 3 uhgrspan1lem1 ⊢ ( ( 𝑉 ∖ { 𝑁 } ) ∈ V ∧ ( 𝐼 ↾ 𝐹 ) ∈ V )
7 opiedgfv ⊢ ( ( ( 𝑉 ∖ { 𝑁 } ) ∈ V ∧ ( 𝐼 ↾ 𝐹 ) ∈ V ) → ( iEdg ‘ ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( 𝐼 ↾ 𝐹 ) ⟩ ) = ( 𝐼 ↾ 𝐹 ) )
8 6 7 ax-mp ⊢ ( iEdg ‘ ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( 𝐼 ↾ 𝐹 ) ⟩ ) = ( 𝐼 ↾ 𝐹 )
9 5 8 eqtri ⊢ ( iEdg ‘ 𝑆 ) = ( 𝐼 ↾ 𝐹 )