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

Metamath Proof Explorer

Theorem umgrspan

Description: A spanning subgraph S of a multigraph G is a multigraph. (Contributed by AV, 27-Nov-2020)

Ref Expression
Hypotheses uhgrspan.v ⊢ V = Vtx ⁡ G
uhgrspan.e ⊢ E = iEdg ⁡ G
uhgrspan.s ⊢ φ → S ∈ W
uhgrspan.q ⊢ φ → Vtx ⁡ S = V
uhgrspan.r ⊢ φ → iEdg ⁡ S = E ↾ A
umgrspan.g ⊢ φ → G ∈ UMGraph
Assertion umgrspan ⊢ φ → S ∈ UMGraph

Proof

Step Hyp Ref Expression
1 uhgrspan.v ⊢ V = Vtx ⁡ G
2 uhgrspan.e ⊢ E = iEdg ⁡ G
3 uhgrspan.s ⊢ φ → S ∈ W
4 uhgrspan.q ⊢ φ → Vtx ⁡ S = V
5 uhgrspan.r ⊢ φ → iEdg ⁡ S = E ↾ A
6 umgrspan.g ⊢ φ → G ∈ UMGraph
7 umgruhgr ⊢ G ∈ UMGraph → G ∈ UHGraph
8 6 7 syl ⊢ φ → G ∈ UHGraph
9 1 2 3 4 5 8 uhgrspansubgr ⊢ φ → S SubGraph G
10 subumgr ⊢ G ∈ UMGraph ∧ S SubGraph G → S ∈ UMGraph
11 6 9 10 syl2anc ⊢ φ → S ∈ UMGraph