Metamath Proof Explorer

Theorem cusgrres

Description: Restricting a complete simple graph. (Contributed by Alexander van der Vekens, 2-Jan-2018)

Ref Expression
Hypotheses cusgrres.v 
|- V = ( Vtx ` G )
cusgrres.e 
|- E = ( Edg ` G )
cusgrres.f 
|- F = { e e. E | N e/ e }
cusgrres.s 
|- S = <. ( V \ { N } ) , ( _I |` F ) >.
Assertion cusgrres 
|- ( ( G e. ComplUSGraph /\ N e. V ) -> S e. ComplUSGraph )

Proof

Step Hyp Ref Expression
1 cusgrres.v 
 |-  V = ( Vtx ` G )
2 cusgrres.e 
 |-  E = ( Edg ` G )
3 cusgrres.f 
 |-  F = { e e. E | N e/ e }
4 cusgrres.s 
 |-  S = <. ( V \ { N } ) , ( _I |` F ) >.
5 cusgrusgr 
 |-  ( G e. ComplUSGraph -> G e. USGraph )
6 1 2 3 4 usgrres1 
 |-  ( ( G e. USGraph /\ N e. V ) -> S e. USGraph )
7 5 6 sylan 
 |-  ( ( G e. ComplUSGraph /\ N e. V ) -> S e. USGraph )
8 iscusgr 
 |-  ( G e. ComplUSGraph <-> ( G e. USGraph /\ G e. ComplGraph ) )
9 usgrupgr 
 |-  ( G e. USGraph -> G e. UPGraph )
10 9 adantr 
 |-  ( ( G e. USGraph /\ G e. ComplGraph ) -> G e. UPGraph )
11 10 anim1i 
 |-  ( ( ( G e. USGraph /\ G e. ComplGraph ) /\ N e. V ) -> ( G e. UPGraph /\ N e. V ) )
12 11 anim1i 
 |-  ( ( ( ( G e. USGraph /\ G e. ComplGraph ) /\ N e. V ) /\ v e. ( V \ { N } ) ) -> ( ( G e. UPGraph /\ N e. V ) /\ v e. ( V \ { N } ) ) )
13 1 iscplgr 
 |-  ( G e. USGraph -> ( G e. ComplGraph <-> A. n e. V n e. ( UnivVtx ` G ) ) )
14 eldifi 
 |-  ( v e. ( V \ { N } ) -> v e. V )
15 14 ad2antll 
 |-  ( ( G e. USGraph /\ ( N e. V /\ v e. ( V \ { N } ) ) ) -> v e. V )
16 eleq1w 
 |-  ( n = v -> ( n e. ( UnivVtx ` G ) <-> v e. ( UnivVtx ` G ) ) )
17 16 rspcv 
 |-  ( v e. V -> ( A. n e. V n e. ( UnivVtx ` G ) -> v e. ( UnivVtx ` G ) ) )
18 15 17 syl 
 |-  ( ( G e. USGraph /\ ( N e. V /\ v e. ( V \ { N } ) ) ) -> ( A. n e. V n e. ( UnivVtx ` G ) -> v e. ( UnivVtx ` G ) ) )
19 18 ex 
 |-  ( G e. USGraph -> ( ( N e. V /\ v e. ( V \ { N } ) ) -> ( A. n e. V n e. ( UnivVtx ` G ) -> v e. ( UnivVtx ` G ) ) ) )
20 19 com23 
 |-  ( G e. USGraph -> ( A. n e. V n e. ( UnivVtx ` G ) -> ( ( N e. V /\ v e. ( V \ { N } ) ) -> v e. ( UnivVtx ` G ) ) ) )
21 13 20 sylbid 
 |-  ( G e. USGraph -> ( G e. ComplGraph -> ( ( N e. V /\ v e. ( V \ { N } ) ) -> v e. ( UnivVtx ` G ) ) ) )
22 21 imp 
 |-  ( ( G e. USGraph /\ G e. ComplGraph ) -> ( ( N e. V /\ v e. ( V \ { N } ) ) -> v e. ( UnivVtx ` G ) ) )
23 22 impl 
 |-  ( ( ( ( G e. USGraph /\ G e. ComplGraph ) /\ N e. V ) /\ v e. ( V \ { N } ) ) -> v e. ( UnivVtx ` G ) )
24 1 2 3 4 uvtxupgrres 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ v e. ( V \ { N } ) ) -> ( v e. ( UnivVtx ` G ) -> v e. ( UnivVtx ` S ) ) )
25 12 23 24 sylc 
 |-  ( ( ( ( G e. USGraph /\ G e. ComplGraph ) /\ N e. V ) /\ v e. ( V \ { N } ) ) -> v e. ( UnivVtx ` S ) )
26 25 ralrimiva 
 |-  ( ( ( G e. USGraph /\ G e. ComplGraph ) /\ N e. V ) -> A. v e. ( V \ { N } ) v e. ( UnivVtx ` S ) )
27 8 26 sylanb 
 |-  ( ( G e. ComplUSGraph /\ N e. V ) -> A. v e. ( V \ { N } ) v e. ( UnivVtx ` S ) )
28 opex 
 |-  <. ( V \ { N } ) , ( _I |` F ) >. e. _V
29 4 28 eqeltri 
 |-  S e. _V
30 1 2 3 4 upgrres1lem2 
 |-  ( Vtx ` S ) = ( V \ { N } )
31 30 eqcomi 
 |-  ( V \ { N } ) = ( Vtx ` S )
32 31 iscplgr 
 |-  ( S e. _V -> ( S e. ComplGraph <-> A. v e. ( V \ { N } ) v e. ( UnivVtx ` S ) ) )
33 29 32 mp1i 
 |-  ( ( G e. ComplUSGraph /\ N e. V ) -> ( S e. ComplGraph <-> A. v e. ( V \ { N } ) v e. ( UnivVtx ` S ) ) )
34 27 33 mpbird 
 |-  ( ( G e. ComplUSGraph /\ N e. V ) -> S e. ComplGraph )
35 iscusgr 
 |-  ( S e. ComplUSGraph <-> ( S e. USGraph /\ S e. ComplGraph ) )
36 7 34 35 sylanbrc 
 |-  ( ( G e. ComplUSGraph /\ N e. V ) -> S e. ComplUSGraph )