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

Metamath Proof Explorer

Theorem usgrspan

Description: A spanning subgraph S of a simple graph G is a simple graph. (Contributed by AV, 15-Oct-2020) (Revised by AV, 16-Oct-2020) (Proof shortened by AV, 18-Nov-2020)

		Ref	Expression
	Hypotheses	uhgrspan.v	$⊢ V = Vtx (G)$
		uhgrspan.e	$⊢ E = iEdg (G)$
		uhgrspan.s	$⊢ φ \to S \in W$
		uhgrspan.q	$⊢ φ \to Vtx (S) = V$
		uhgrspan.r	$⊢ φ \to iEdg (S) = {E ↾}_{A}$
		usgrspan.g	$⊢ φ \to G \in USGraph$
	Assertion	usgrspan	$⊢ φ \to S \in USGraph$

Proof

Step	Hyp	Ref	Expression
1		uhgrspan.v	$⊢ V = Vtx (G)$
2		uhgrspan.e	$⊢ E = iEdg (G)$
3		uhgrspan.s	$⊢ φ \to S \in W$
4		uhgrspan.q	$⊢ φ \to Vtx (S) = V$
5		uhgrspan.r	$⊢ φ \to iEdg (S) = {E ↾}_{A}$
6		usgrspan.g	$⊢ φ \to G \in USGraph$
7		usgruhgr	$⊢ G \in USGraph \to G \in UHGraph$
8	6 7	syl	$⊢ φ \to G \in UHGraph$
9	1 2 3 4 5 8	uhgrspansubgr	$⊢ φ \to S SubGraph G$
10		subusgr	$⊢ (G \in USGraph \land S SubGraph G) \to S \in USGraph$
11	6 9 10	syl2anc	$⊢ φ \to S \in USGraph$