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

Metamath Proof Explorer

Theorem uhgrspan1lem3

Description: Lemma 3 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
uhgrspan1.s ⊢ S = V ∖ N I ↾ F
Assertion uhgrspan1lem3 ⊢ iEdg ⁡ S = I ↾ F

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 uhgrspan1.s ⊢ S = V ∖ N I ↾ F
5 4 fveq2i ⊢ iEdg ⁡ S = iEdg ⁡ V ∖ N I ↾ F
6 1 2 3 uhgrspan1lem1 ⊢ V ∖ N ∈ V ∧ I ↾ F ∈ V
7 opiedgfv ⊢ V ∖ N ∈ V ∧ I ↾ F ∈ V → iEdg ⁡ V ∖ N I ↾ F = I ↾ F
8 6 7 ax-mp ⊢ iEdg ⁡ V ∖ N I ↾ F = I ↾ F
9 5 8 eqtri ⊢ iEdg ⁡ S = I ↾ F