Theorem uhgrspansubgr

Description: A spanning subgraph S of a hypergraph G is actually a subgraph of G . A subgraph S of a graph G which has the same vertices as G and is obtained by removing some edges of G is called aspanning subgraph (see section I.1 in Bollobas p. 2 and section 1.1 in Diestel p. 4). Formally, the edges are "removed" by restricting the edge function of the original graph by an arbitrary class (which actually needs not to be a subset of the domain of the edge function). (Contributed by AV, 18-Nov-2020) (Proof shortened by AV, 21-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 ) )
	uhgrspan.g	|- ( ph -> G e. UHGraph )
Assertion	uhgrspansubgr	|- ( ph -> S SubGraph G )

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		uhgrspan.g	|- ( ph -> G e. UHGraph )
7		ssid	|- ( Vtx ` S ) C_ ( Vtx ` S )
8	7 4	sseqtrid	|- ( ph -> ( Vtx ` S ) C_ V )
9		resss	|- ( E |` A ) C_ E
10	5 9	eqsstrdi	|- ( ph -> ( iEdg ` S ) C_ E )
11	1 2 3 4 5 6	uhgrspansubgrlem	|- ( ph -> ( Edg ` S ) C_ ~P ( Vtx ` S ) )
12	2	uhgrfun	|- ( G e. UHGraph -> Fun E )
13	6 12	syl	|- ( ph -> Fun E )
14		eqid	|- ( Vtx ` S ) = ( Vtx ` S )
15		eqid	|- ( iEdg ` S ) = ( iEdg ` S )
16		eqid	|- ( Edg ` S ) = ( Edg ` S )
17	14 1 15 2 16	issubgr2	|- ( ( G e. UHGraph /\ Fun E /\ S e. W ) -> ( S SubGraph G <-> ( ( Vtx ` S ) C_ V /\ ( iEdg ` S ) C_ E /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) ) )
18	6 13 3 17	syl3anc	|- ( ph -> ( S SubGraph G <-> ( ( Vtx ` S ) C_ V /\ ( iEdg ` S ) C_ E /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) ) )
19	8 10 11 18	mpbir3and	|- ( ph -> S SubGraph G )