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	|- ( ph -> S e. W )
	uhgrspan.q	|- ( ph -> ( Vtx ` S ) = V )
	uhgrspan.r	|- ( ph -> ( iEdg ` S ) = ( E |` A ) )
	usgrspan.g	|- ( ph -> G e. USGraph )
Assertion	usgrspan	|- ( ph -> S e. USGraph )

Proof

Step	Hyp	Ref	Expression
1		uhgrspan.v	|- V = ( Vtx ` G )
2		uhgrspan.e	|- E = ( iEdg ` G )
3		uhgrspan.s	|- ( ph -> S e. W )
4		uhgrspan.q	|- ( ph -> ( Vtx ` S ) = V )
5		uhgrspan.r	|- ( ph -> ( iEdg ` S ) = ( E |` A ) )
6		usgrspan.g	|- ( ph -> G e. USGraph )
7		usgruhgr	|- ( G e. USGraph -> G e. UHGraph )
8	6 7	syl	|- ( ph -> G e. UHGraph )
9	1 2 3 4 5 8	uhgrspansubgr	|- ( ph -> S SubGraph G )
10		subusgr	|- ( ( G e. USGraph /\ S SubGraph G ) -> S e. USGraph )
11	6 9 10	syl2anc	|- ( ph -> S e. USGraph )