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

Metamath Proof Explorer

Theorem upgrres1lem1

Description: Lemma 1 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
Assertion upgrres1lem1 ⊢ V ∖ N ∈ V ∧ I ↾ F ∈ V

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 1 fvexi ⊢ V ∈ V
5 4 difexi ⊢ V ∖ N ∈ V
6 2 fvexi ⊢ E ∈ V
7 3 6 rabex2 ⊢ F ∈ V
8 resiexg ⊢ F ∈ V → I ↾ F ∈ V
9 7 8 ax-mp ⊢ I ↾ F ∈ V
10 5 9 pm3.2i ⊢ V ∖ N ∈ V ∧ I ↾ F ∈ V