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

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 ↾ 𝐹 )