Metamath Proof Explorer

Theorem upgrspanop

Description: A spanning subgraph of a pseudograph represented by an ordered pair is a pseudograph. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 13-Oct-2020)

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

Proof

Step Hyp Ref Expression
1 uhgrspanop.v 
 |-  V = ( Vtx ` G )
2 uhgrspanop.e 
 |-  E = ( iEdg ` G )
3 vex 
 |-  g e. _V
4 3 a1i 
 |-  ( ( G e. UPGraph /\ ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = ( E |` A ) ) ) -> g e. _V )
5 simprl 
 |-  ( ( G e. UPGraph /\ ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = ( E |` A ) ) ) -> ( Vtx ` g ) = V )
6 simprr 
 |-  ( ( G e. UPGraph /\ ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = ( E |` A ) ) ) -> ( iEdg ` g ) = ( E |` A ) )
7 simpl 
 |-  ( ( G e. UPGraph /\ ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = ( E |` A ) ) ) -> G e. UPGraph )
8 1 2 4 5 6 7 upgrspan 
 |-  ( ( G e. UPGraph /\ ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = ( E |` A ) ) ) -> g e. UPGraph )
9 8 ex 
 |-  ( G e. UPGraph -> ( ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = ( E |` A ) ) -> g e. UPGraph ) )
10 9 alrimiv 
 |-  ( G e. UPGraph -> A. g ( ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = ( E |` A ) ) -> g e. UPGraph ) )
11 1 fvexi 
 |-  V e. _V
12 11 a1i 
 |-  ( G e. UPGraph -> V e. _V )
13 2 fvexi 
 |-  E e. _V
14 13 resex 
 |-  ( E |` A ) e. _V
15 14 a1i 
 |-  ( G e. UPGraph -> ( E |` A ) e. _V )
16 10 12 15 gropeld 
 |-  ( G e. UPGraph -> <. V , ( E |` A ) >. e. UPGraph )