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 ‘ 𝑆 ) = ( 𝐼𝐹 )