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 )