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

Metamath Proof Explorer

Theorem upgrspan

Description: A spanning subgraph S of a pseudograph G is a pseudograph. (Contributed by AV, 11-Oct-2020) (Proof shortened by AV, 18-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
upgrspan.g ⊢ φ → G ∈ UPGraph
Assertion upgrspan ⊢ φ → S ∈ UPGraph

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 upgrspan.g ⊢ φ → G ∈ UPGraph
7 upgruhgr ⊢ G ∈ UPGraph → G ∈ UHGraph
8 6 7 syl ⊢ φ → G ∈ UHGraph
9 1 2 3 4 5 8 uhgrspansubgr ⊢ φ → S SubGraph G
10 subupgr ⊢ G ∈ UPGraph ∧ S SubGraph G → S ∈ UPGraph
11 6 9 10 syl2anc ⊢ φ → S ∈ UPGraph