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

Metamath Proof Explorer

Theorem uhgrspan1lem1

Description: Lemma 1 for uhgrspan1 . (Contributed by AV, 19-Nov-2020)

Ref Expression
Hypotheses uhgrspan1.v ⊢ V = Vtx ⁡ G
uhgrspan1.i ⊢ I = iEdg ⁡ G
uhgrspan1.f ⊢ F = i ∈ dom ⁡ I | N ∉ I ⁡ i
Assertion uhgrspan1lem1 ⊢ V ∖ N ∈ V ∧ I ↾ F ∈ V

Proof

Step Hyp Ref Expression
1 uhgrspan1.v ⊢ V = Vtx ⁡ G
2 uhgrspan1.i ⊢ I = iEdg ⁡ G
3 uhgrspan1.f ⊢ F = i ∈ dom ⁡ I | N ∉ I ⁡ i
4 1 fvexi ⊢ V ∈ V
5 4 difexi ⊢ V ∖ N ∈ V
6 2 fvexi ⊢ I ∈ V
7 6 resex ⊢ I ↾ F ∈ V
8 5 7 pm3.2i ⊢ V ∖ N ∈ V ∧ I ↾ F ∈ V