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

Metamath Proof Explorer

Theorem cusgrexg

Description: For each set there is a set of edges so that the set together with these edges is a complete simple graph. (Contributed by Alexander van der Vekens, 12-Jan-2018) (Revised by AV, 5-Nov-2020)

Ref Expression
Assertion cusgrexg 
|- ( V e. W -> E. e <. V , e >. e. ComplUSGraph )

Proof

Step Hyp Ref Expression
1 fveqeq2 
 |-  ( y = x -> ( ( # ` y ) = 2 <-> ( # ` x ) = 2 ) )
2 1 cbvrabv 
 |-  { y e. ~P V | ( # ` y ) = 2 } = { x e. ~P V | ( # ` x ) = 2 }
3 2 cusgrexilem1 
 |-  ( V e. W -> ( _I |` { y e. ~P V | ( # ` y ) = 2 } ) e. _V )
4 2 cusgrexi 
 |-  ( V e. W -> <. V , ( _I |` { y e. ~P V | ( # ` y ) = 2 } ) >. e. ComplUSGraph )
5 opeq2 
 |-  ( e = ( _I |` { y e. ~P V | ( # ` y ) = 2 } ) -> <. V , e >. = <. V , ( _I |` { y e. ~P V | ( # ` y ) = 2 } ) >. )
6 5 eleq1d 
 |-  ( e = ( _I |` { y e. ~P V | ( # ` y ) = 2 } ) -> ( <. V , e >. e. ComplUSGraph <-> <. V , ( _I |` { y e. ~P V | ( # ` y ) = 2 } ) >. e. ComplUSGraph ) )
7 3 4 6 spcedv 
 |-  ( V e. W -> E. e <. V , e >. e. ComplUSGraph )