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

Metamath Proof Explorer

Theorem upgrres1lem2

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

Ref Expression
Hypotheses upgrres1.v ⊢ V = Vtx ⁡ G
upgrres1.e ⊢ E = Edg ⁡ G
upgrres1.f ⊢ F = e ∈ E | N ∉ e
upgrres1.s ⊢ S = V ∖ N I ↾ F
Assertion upgrres1lem2 ⊢ Vtx ⁡ S = V ∖ N

Proof

Step Hyp Ref Expression
1 upgrres1.v ⊢ V = Vtx ⁡ G
2 upgrres1.e ⊢ E = Edg ⁡ G
3 upgrres1.f ⊢ F = e ∈ E | N ∉ e
4 upgrres1.s ⊢ S = V ∖ N I ↾ F
5 4 fveq2i ⊢ Vtx ⁡ S = Vtx ⁡ V ∖ N I ↾ F
6 1 2 3 upgrres1lem1 ⊢ V ∖ N ∈ V ∧ I ↾ F ∈ V
7 opvtxfv ⊢ V ∖ N ∈ V ∧ I ↾ F ∈ V → Vtx ⁡ V ∖ N I ↾ F = V ∖ N
8 6 7 ax-mp ⊢ Vtx ⁡ V ∖ N I ↾ F = V ∖ N
9 5 8 eqtri ⊢ Vtx ⁡ S = V ∖ N