Theorem uhgrspanop

Description: A spanning subgraph of a hypergraph represented by an ordered pair is a hypergraph. (Contributed by Alexander van der Vekens, 27-Dec-2017) (Revised by AV, 11-Oct-2020)

	Ref	Expression
Hypotheses	uhgrspanop.v	|- V = ( Vtx ` G )
	uhgrspanop.e	|- E = ( iEdg ` G )
Assertion	uhgrspanop	|- ( G e. UHGraph -> <. V , ( E |` A ) >. e. UHGraph )

Proof

Step	Hyp	Ref	Expression
1		uhgrspanop.v	|- V = ( Vtx ` G )
2		uhgrspanop.e	|- E = ( iEdg ` G )
3		opex	|- <. V , ( E |` A ) >. e. _V
4	3	a1i	|- ( G e. UHGraph -> <. V , ( E |` A ) >. e. _V )
5	1	fvexi	|- V e. _V
6	2	fvexi	|- E e. _V
7	6	resex	|- ( E |` A ) e. _V
8	5 7	opvtxfvi	|- ( Vtx ` <. V , ( E |` A ) >. ) = V
9	8	a1i	|- ( G e. UHGraph -> ( Vtx ` <. V , ( E |` A ) >. ) = V )
10	5 7	opiedgfvi	|- ( iEdg ` <. V , ( E |` A ) >. ) = ( E |` A )
11	10	a1i	|- ( G e. UHGraph -> ( iEdg ` <. V , ( E |` A ) >. ) = ( E |` A ) )
12		id	|- ( G e. UHGraph -> G e. UHGraph )
13	1 2 4 9 11 12	uhgrspan	|- ( G e. UHGraph -> <. V , ( E |` A ) >. e. UHGraph )