Metamath Proof Explorer


Theorem upgrres1lem3

Description: Lemma 3 for upgrres1 . (Contributed by AV, 7-Nov-2020)

Ref Expression
Hypotheses upgrres1.v 𝑉 = ( Vtx ‘ 𝐺 )
upgrres1.e 𝐸 = ( Edg ‘ 𝐺 )
upgrres1.f 𝐹 = { 𝑒𝐸𝑁𝑒 }
upgrres1.s 𝑆 = ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( I ↾ 𝐹 ) ⟩
Assertion upgrres1lem3 ( iEdg ‘ 𝑆 ) = ( I ↾ 𝐹 )

Proof

Step Hyp Ref Expression
1 upgrres1.v 𝑉 = ( Vtx ‘ 𝐺 )
2 upgrres1.e 𝐸 = ( Edg ‘ 𝐺 )
3 upgrres1.f 𝐹 = { 𝑒𝐸𝑁𝑒 }
4 upgrres1.s 𝑆 = ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( I ↾ 𝐹 ) ⟩
5 4 fveq2i ( iEdg ‘ 𝑆 ) = ( iEdg ‘ ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( I ↾ 𝐹 ) ⟩ )
6 1 2 3 upgrres1lem1 ( ( 𝑉 ∖ { 𝑁 } ) ∈ V ∧ ( I ↾ 𝐹 ) ∈ V )
7 opiedgfv ( ( ( 𝑉 ∖ { 𝑁 } ) ∈ V ∧ ( I ↾ 𝐹 ) ∈ V ) → ( iEdg ‘ ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( I ↾ 𝐹 ) ⟩ ) = ( I ↾ 𝐹 ) )
8 6 7 ax-mp ( iEdg ‘ ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( I ↾ 𝐹 ) ⟩ ) = ( I ↾ 𝐹 )
9 5 8 eqtri ( iEdg ‘ 𝑆 ) = ( I ↾ 𝐹 )