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 h v h E ∃! w V h v w E

Proof

Step Hyp Ref Expression
1 ral0 v v A E ∃! w A A v w 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 v A E
8 reueq1 A h = A A ∃! w A h v w E ∃! w A A v w E
9 3 8 syl h = A ∃! w A h v w E ∃! w A A v w E
10 7 9 anbi12d h = A v h E ∃! w A h v w E v A E ∃! w A A v w E
11 5 10 raleqbidv h = A v A h v h E ∃! w A h v w E v v A E ∃! w A A v w E
12 11 rexsng A X h A v A h v h E ∃! w A h v w E v v A E ∃! w A A v w E
13 1 12 mpbiri A X h A v A h v h E ∃! w A h v w E
14 13 adantr A X V = A h A v A h v h E ∃! w A h v w E
15 difeq1 V = A V h = A h
16 reueq1 V h = A h ∃! w V h v w E ∃! w A h v w E
17 15 16 syl V = A ∃! w V h v w E ∃! w A h v w E
18 17 anbi2d V = A v h E ∃! w V h v w E v h E ∃! w A h v w E
19 15 18 raleqbidv V = A v V h v h E ∃! w V h v w E v A h v h E ∃! w A h v w E
20 19 rexeqbi1dv V = A h V v V h v h E ∃! w V h v w E h A v A h v h E ∃! w A h v w E
21 20 adantl A X V = A h V v V h v h E ∃! w V h v w E h A v A h v h E ∃! w A h v w E
22 14 21 mpbird A X V = A h V v V h v h E ∃! w V h v w E