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

Metamath Proof Explorer

Theorem uhgrspan

Description: A spanning subgraph S of a hypergraph G is a hypergraph. (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
uhgrspan.g ⊢ φ → G ∈ UHGraph
Assertion uhgrspan ⊢ φ → S ∈ UHGraph

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 uhgrspan.g ⊢ φ → G ∈ UHGraph
7 1 2 3 4 5 6 uhgrspansubgr ⊢ φ → S SubGraph G
8 subuhgr ⊢ G ∈ UHGraph ∧ S SubGraph G → S ∈ UHGraph
9 6 7 8 syl2anc ⊢ φ → S ∈ UHGraph