Metamath Proof Explorer

Theorem 1to2vfriswmgr

Description: Every friendship graph with one or two vertices is a windmill graph. (Contributed by Alexander van der Vekens, 6-Oct-2017) (Revised by AV, 31-Mar-2021)

Ref Expression
Hypotheses 3vfriswmgr.v ⊢ V = Vtx ⁡ G
3vfriswmgr.e ⊢ E = Edg ⁡ G
Assertion 1to2vfriswmgr ⊢ A ∈ X ∧ V = A ∨ V = A B → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E

Proof

Step Hyp Ref Expression
1 3vfriswmgr.v ⊢ V = Vtx ⁡ G
2 3vfriswmgr.e ⊢ E = Edg ⁡ G
3 1vwmgr ⊢ A ∈ X ∧ V = A → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
4 3 a1d ⊢ A ∈ X ∧ V = A → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
5 4 expcom ⊢ V = A → A ∈ X → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
6 simpr ⊢ B ∈ V ∧ A ≠ B ∧ A ∈ X → A ∈ X
7 simpll ⊢ B ∈ V ∧ A ≠ B ∧ A ∈ X → B ∈ V
8 simplr ⊢ B ∈ V ∧ A ≠ B ∧ A ∈ X → A ≠ B
9 6 7 8 3jca ⊢ B ∈ V ∧ A ≠ B ∧ A ∈ X → A ∈ X ∧ B ∈ V ∧ A ≠ B
10 1 eqeq1i ⊢ V = A B ↔ Vtx ⁡ G = A B
11 10 biimpi ⊢ V = A B → Vtx ⁡ G = A B
12 nfrgr2v ⊢ A ∈ X ∧ B ∈ V ∧ A ≠ B ∧ Vtx ⁡ G = A B → G ∉ FriendGraph
13 9 11 12 syl2anr ⊢ V = A B ∧ B ∈ V ∧ A ≠ B ∧ A ∈ X → G ∉ FriendGraph
14 df-nel ⊢ G ∉ FriendGraph ↔ ¬ G ∈ FriendGraph
15 13 14 sylib ⊢ V = A B ∧ B ∈ V ∧ A ≠ B ∧ A ∈ X → ¬ G ∈ FriendGraph
16 15 pm2.21d ⊢ V = A B ∧ B ∈ V ∧ A ≠ B ∧ A ∈ X → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
17 16 expcom ⊢ B ∈ V ∧ A ≠ B ∧ A ∈ X → V = A B → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
18 17 ex ⊢ B ∈ V ∧ A ≠ B → A ∈ X → V = A B → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
19 18 com23 ⊢ B ∈ V ∧ A ≠ B → V = A B → A ∈ X → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
20 ianor ⊢ ¬ B ∈ V ∧ A ≠ B ↔ ¬ B ∈ V ∨ ¬ A ≠ B
21 prprc2 ⊢ ¬ B ∈ V → A B = A
22 nne ⊢ ¬ A ≠ B ↔ A = B
23 preq2 ⊢ B = A → A B = A A
24 23 eqcoms ⊢ A = B → A B = A A
25 dfsn2 ⊢ A = A A
26 24 25 eqtr4di ⊢ A = B → A B = A
27 22 26 sylbi ⊢ ¬ A ≠ B → A B = A
28 21 27 jaoi ⊢ ¬ B ∈ V ∨ ¬ A ≠ B → A B = A
29 20 28 sylbi ⊢ ¬ B ∈ V ∧ A ≠ B → A B = A
30 29 eqeq2d ⊢ ¬ B ∈ V ∧ A ≠ B → V = A B ↔ V = A
31 30 5 syl6bi ⊢ ¬ B ∈ V ∧ A ≠ B → V = A B → A ∈ X → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
32 19 31 pm2.61i ⊢ V = A B → A ∈ X → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
33 5 32 jaoi ⊢ V = A ∨ V = A B → A ∈ X → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
34 33 impcom ⊢ A ∈ X ∧ V = A ∨ V = A B → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E