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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	uhgrspan.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
	uhgrspan.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
	uhgrspan.q	⊢ ( 𝜑 → ( Vtx ‘ 𝑆 ) = 𝑉 )
	uhgrspan.r	⊢ ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( 𝐸 ↾ 𝐴 ) )
	usgrspan.g	⊢ ( 𝜑 → 𝐺 ∈ USGraph )
Assertion	usgrspan	⊢ ( 𝜑 → 𝑆 ∈ USGraph )

Proof

Step	Hyp	Ref	Expression
1		uhgrspan.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		uhgrspan.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3		uhgrspan.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
4		uhgrspan.q	⊢ ( 𝜑 → ( Vtx ‘ 𝑆 ) = 𝑉 )
5		uhgrspan.r	⊢ ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( 𝐸 ↾ 𝐴 ) )
6		usgrspan.g	⊢ ( 𝜑 → 𝐺 ∈ USGraph )
7		usgruhgr	⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UHGraph )
8	6 7	syl	⊢ ( 𝜑 → 𝐺 ∈ UHGraph )
9	1 2 3 4 5 8	uhgrspansubgr	⊢ ( 𝜑 → 𝑆 SubGraph 𝐺 )
10		subusgr	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑆 SubGraph 𝐺 ) → 𝑆 ∈ USGraph )
11	6 9 10	syl2anc	⊢ ( 𝜑 → 𝑆 ∈ USGraph )