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

Metamath Proof Explorer

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 )