Theorem 1vwmgr

Description: Every graph with one vertex (which may be connect with itself by (multiple) loops!) is a windmill graph. (Contributed by Alexander van der Vekens, 5-Oct-2017) (Revised by AV, 31-Mar-2021)

	Ref	Expression
Assertion	1vwmgr	|- ( ( A e. X /\ V = { A } ) -> E. h e. V A. v e. ( V \ { h } ) ( { v , h } e. E /\ E! w e. ( V \ { h } ) { v , w } e. E ) )

Proof

Step	Hyp	Ref	Expression
1		ral0	|- A. v e. (/) ( { v , A } e. E /\ E! w e. ( { A } \ { A } ) { v , w } e. E )
2		sneq	|- ( h = A -> { h } = { A } )
3	2	difeq2d	|- ( h = A -> ( { A } \ { h } ) = ( { A } \ { A } ) )
4		difid	|- ( { A } \ { A } ) = (/)
5	3 4	eqtrdi	|- ( h = A -> ( { A } \ { h } ) = (/) )
6		preq2	|- ( h = A -> { v , h } = { v , A } )
7	6	eleq1d	|- ( h = A -> ( { v , h } e. E <-> { v , A } e. E ) )
8		reueq1	|- ( ( { A } \ { h } ) = ( { A } \ { A } ) -> ( E! w e. ( { A } \ { h } ) { v , w } e. E <-> E! w e. ( { A } \ { A } ) { v , w } e. E ) )
9	3 8	syl	|- ( h = A -> ( E! w e. ( { A } \ { h } ) { v , w } e. E <-> E! w e. ( { A } \ { A } ) { v , w } e. E ) )
10	7 9	anbi12d	|- ( h = A -> ( ( { v , h } e. E /\ E! w e. ( { A } \ { h } ) { v , w } e. E ) <-> ( { v , A } e. E /\ E! w e. ( { A } \ { A } ) { v , w } e. E ) ) )
11	5 10	raleqbidv	|- ( h = A -> ( A. v e. ( { A } \ { h } ) ( { v , h } e. E /\ E! w e. ( { A } \ { h } ) { v , w } e. E ) <-> A. v e. (/) ( { v , A } e. E /\ E! w e. ( { A } \ { A } ) { v , w } e. E ) ) )
12	11	rexsng	|- ( A e. X -> ( E. h e. { A } A. v e. ( { A } \ { h } ) ( { v , h } e. E /\ E! w e. ( { A } \ { h } ) { v , w } e. E ) <-> A. v e. (/) ( { v , A } e. E /\ E! w e. ( { A } \ { A } ) { v , w } e. E ) ) )
13	1 12	mpbiri	|- ( A e. X -> E. h e. { A } A. v e. ( { A } \ { h } ) ( { v , h } e. E /\ E! w e. ( { A } \ { h } ) { v , w } e. E ) )
14	13	adantr	|- ( ( A e. X /\ V = { A } ) -> E. h e. { A } A. v e. ( { A } \ { h } ) ( { v , h } e. E /\ E! w e. ( { A } \ { h } ) { v , w } e. E ) )
15		difeq1	|- ( V = { A } -> ( V \ { h } ) = ( { A } \ { h } ) )
16		reueq1	|- ( ( V \ { h } ) = ( { A } \ { h } ) -> ( E! w e. ( V \ { h } ) { v , w } e. E <-> E! w e. ( { A } \ { h } ) { v , w } e. E ) )
17	15 16	syl	|- ( V = { A } -> ( E! w e. ( V \ { h } ) { v , w } e. E <-> E! w e. ( { A } \ { h } ) { v , w } e. E ) )
18	17	anbi2d	|- ( V = { A } -> ( ( { v , h } e. E /\ E! w e. ( V \ { h } ) { v , w } e. E ) <-> ( { v , h } e. E /\ E! w e. ( { A } \ { h } ) { v , w } e. E ) ) )
19	15 18	raleqbidv	|- ( V = { A } -> ( A. v e. ( V \ { h } ) ( { v , h } e. E /\ E! w e. ( V \ { h } ) { v , w } e. E ) <-> A. v e. ( { A } \ { h } ) ( { v , h } e. E /\ E! w e. ( { A } \ { h } ) { v , w } e. E ) ) )
20	19	rexeqbi1dv	|- ( V = { A } -> ( E. h e. V A. v e. ( V \ { h } ) ( { v , h } e. E /\ E! w e. ( V \ { h } ) { v , w } e. E ) <-> E. h e. { A } A. v e. ( { A } \ { h } ) ( { v , h } e. E /\ E! w e. ( { A } \ { h } ) { v , w } e. E ) ) )
21	20	adantl	|- ( ( A e. X /\ V = { A } ) -> ( E. h e. V A. v e. ( V \ { h } ) ( { v , h } e. E /\ E! w e. ( V \ { h } ) { v , w } e. E ) <-> E. h e. { A } A. v e. ( { A } \ { h } ) ( { v , h } e. E /\ E! w e. ( { A } \ { h } ) { v , w } e. E ) ) )
22	14 21	mpbird	|- ( ( A e. X /\ V = { A } ) -> E. h e. V A. v e. ( V \ { h } ) ( { v , h } e. E /\ E! w e. ( V \ { h } ) { v , w } e. E ) )