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