Metamath Proof Explorer

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∈X∧V=A→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E

Proof

Step Hyp Ref Expression
1 ral0 ⊢∀v∈∅vA∈E∧∃!w∈A∖Avw∈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→vh=vA
7 6 eleq1d ⊢h=A→vh∈E↔vA∈E
8 reueq1 ⊢A∖h=A∖A→∃!w∈A∖hvw∈E↔∃!w∈A∖Avw∈E
9 3 8 syl ⊢h=A→∃!w∈A∖hvw∈E↔∃!w∈A∖Avw∈E
10 7 9 anbi12d ⊢h=A→vh∈E∧∃!w∈A∖hvw∈E↔vA∈E∧∃!w∈A∖Avw∈E
11 5 10 raleqbidv ⊢h=A→∀v∈A∖hvh∈E∧∃!w∈A∖hvw∈E↔∀v∈∅vA∈E∧∃!w∈A∖Avw∈E
12 11 rexsng ⊢A∈X→∃h∈A∀v∈A∖hvh∈E∧∃!w∈A∖hvw∈E↔∀v∈∅vA∈E∧∃!w∈A∖Avw∈E
13 1 12 mpbiri ⊢A∈X→∃h∈A∀v∈A∖hvh∈E∧∃!w∈A∖hvw∈E
14 13 adantr ⊢A∈X∧V=A→∃h∈A∀v∈A∖hvh∈E∧∃!w∈A∖hvw∈E
15 difeq1 ⊢V=A→V∖h=A∖h
16 reueq1 ⊢V∖h=A∖h→∃!w∈V∖hvw∈E↔∃!w∈A∖hvw∈E
17 15 16 syl ⊢V=A→∃!w∈V∖hvw∈E↔∃!w∈A∖hvw∈E
18 17 anbi2d ⊢V=A→vh∈E∧∃!w∈V∖hvw∈E↔vh∈E∧∃!w∈A∖hvw∈E
19 15 18 raleqbidv ⊢V=A→∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E↔∀v∈A∖hvh∈E∧∃!w∈A∖hvw∈E
20 19 rexeqbi1dv ⊢V=A→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E↔∃h∈A∀v∈A∖hvh∈E∧∃!w∈A∖hvw∈E
21 20 adantl ⊢A∈X∧V=A→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E↔∃h∈A∀v∈A∖hvh∈E∧∃!w∈A∖hvw∈E
22 14 21 mpbird ⊢A∈X∧V=A→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E