Metamath Proof Explorer

Theorem 1to3vfriswmgr

Description: Every friendship graph with one, two or three 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 1to3vfriswmgr ⊢ A ∈ X ∧ V = A ∨ V = A B ∨ V = A B C → 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 df-3or ⊢ V = A ∨ V = A B ∨ V = A B C ↔ V = A ∨ V = A B ∨ V = A B C
4 1 2 1to2vfriswmgr ⊢ A ∈ X ∧ V = A ∨ V = A B → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
5 4 expcom ⊢ V = A ∨ V = A B → A ∈ X → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
6 tppreq3 ⊢ B = C → A B C = A B
7 6 eqeq2d ⊢ B = C → V = A B C ↔ V = A B
8 olc ⊢ V = A B → V = A ∨ V = A B
9 8 anim1ci ⊢ V = A B ∧ A ∈ X → A ∈ X ∧ V = A ∨ V = A B
10 9 4 syl ⊢ V = A B ∧ A ∈ X → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
11 10 ex ⊢ V = A B → A ∈ X → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
12 7 11 syl6bi ⊢ B = C → V = A B C → A ∈ X → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
13 tpprceq3 ⊢ ¬ B ∈ V ∧ B ≠ A → C A B = C A
14 tprot ⊢ C A B = A B C
15 14 eqeq1i ⊢ C A B = C A ↔ A B C = C A
16 15 biimpi ⊢ C A B = C A → A B C = C A
17 prcom ⊢ C A = A C
18 16 17 eqtrdi ⊢ C A B = C A → A B C = A C
19 18 eqeq2d ⊢ C A B = C A → V = A B C ↔ V = A C
20 olc ⊢ V = A C → V = A ∨ V = A C
21 1 2 1to2vfriswmgr ⊢ A ∈ X ∧ V = A ∨ V = A C → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
22 20 21 sylan2 ⊢ A ∈ X ∧ V = A C → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
23 22 expcom ⊢ V = A C → A ∈ X → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
24 19 23 syl6bi ⊢ C A B = C A → V = A B C → A ∈ X → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
25 13 24 syl ⊢ ¬ B ∈ V ∧ B ≠ A → V = A B C → A ∈ X → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
26 25 a1d ⊢ ¬ B ∈ V ∧ B ≠ A → B ≠ C → V = A B C → A ∈ X → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
27 tpprceq3 ⊢ ¬ C ∈ V ∧ C ≠ A → B A C = B A
28 tpcoma ⊢ B A C = A B C
29 28 eqeq1i ⊢ B A C = B A ↔ A B C = B A
30 29 biimpi ⊢ B A C = B A → A B C = B A
31 prcom ⊢ B A = A B
32 30 31 eqtrdi ⊢ B A C = B A → A B C = A B
33 32 eqeq2d ⊢ B A C = B A → V = A B C ↔ V = A B
34 8 4 sylan2 ⊢ A ∈ X ∧ V = A B → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
35 34 expcom ⊢ V = A B → A ∈ X → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
36 35 a1d ⊢ V = A B → B ≠ C → A ∈ X → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
37 33 36 syl6bi ⊢ B A C = B A → V = A B C → B ≠ C → A ∈ X → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
38 27 37 syl ⊢ ¬ C ∈ V ∧ C ≠ A → V = A B C → B ≠ C → A ∈ X → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
39 38 com23 ⊢ ¬ C ∈ V ∧ C ≠ A → B ≠ C → V = A B C → A ∈ X → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
40 simpl ⊢ B ∈ V ∧ B ≠ A → B ∈ V
41 simpl ⊢ C ∈ V ∧ C ≠ A → C ∈ V
42 40 41 anim12i ⊢ B ∈ V ∧ B ≠ A ∧ C ∈ V ∧ C ≠ A → B ∈ V ∧ C ∈ V
43 42 ad2antrr ⊢ B ∈ V ∧ B ≠ A ∧ C ∈ V ∧ C ≠ A ∧ B ≠ C ∧ V = A B C → B ∈ V ∧ C ∈ V
44 43 anim1ci ⊢ B ∈ V ∧ B ≠ A ∧ C ∈ V ∧ C ≠ A ∧ B ≠ C ∧ V = A B C ∧ A ∈ X → A ∈ X ∧ B ∈ V ∧ C ∈ V
45 3anass ⊢ A ∈ X ∧ B ∈ V ∧ C ∈ V ↔ A ∈ X ∧ B ∈ V ∧ C ∈ V
46 44 45 sylibr ⊢ B ∈ V ∧ B ≠ A ∧ C ∈ V ∧ C ≠ A ∧ B ≠ C ∧ V = A B C ∧ A ∈ X → A ∈ X ∧ B ∈ V ∧ C ∈ V
47 simpr ⊢ B ∈ V ∧ B ≠ A → B ≠ A
48 47 necomd ⊢ B ∈ V ∧ B ≠ A → A ≠ B
49 simpr ⊢ C ∈ V ∧ C ≠ A → C ≠ A
50 49 necomd ⊢ C ∈ V ∧ C ≠ A → A ≠ C
51 48 50 anim12i ⊢ B ∈ V ∧ B ≠ A ∧ C ∈ V ∧ C ≠ A → A ≠ B ∧ A ≠ C
52 51 anim1i ⊢ B ∈ V ∧ B ≠ A ∧ C ∈ V ∧ C ≠ A ∧ B ≠ C → A ≠ B ∧ A ≠ C ∧ B ≠ C
53 df-3an ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C ↔ A ≠ B ∧ A ≠ C ∧ B ≠ C
54 52 53 sylibr ⊢ B ∈ V ∧ B ≠ A ∧ C ∈ V ∧ C ≠ A ∧ B ≠ C → A ≠ B ∧ A ≠ C ∧ B ≠ C
55 54 ad2antrr ⊢ B ∈ V ∧ B ≠ A ∧ C ∈ V ∧ C ≠ A ∧ B ≠ C ∧ V = A B C ∧ A ∈ X → A ≠ B ∧ A ≠ C ∧ B ≠ C
56 simplr ⊢ B ∈ V ∧ B ≠ A ∧ C ∈ V ∧ C ≠ A ∧ B ≠ C ∧ V = A B C ∧ A ∈ X → V = A B C
57 1 2 3vfriswmgr ⊢ A ∈ X ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
58 46 55 56 57 syl3anc ⊢ B ∈ V ∧ B ≠ A ∧ C ∈ V ∧ C ≠ A ∧ B ≠ C ∧ V = A B C ∧ A ∈ X → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
59 58 exp41 ⊢ B ∈ V ∧ B ≠ A ∧ C ∈ V ∧ C ≠ A → B ≠ C → V = A B C → A ∈ X → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
60 26 39 59 ecase ⊢ B ≠ C → V = A B C → A ∈ X → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
61 12 60 pm2.61ine ⊢ V = A B C → A ∈ X → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
62 5 61 jaoi ⊢ V = A ∨ V = A B ∨ V = A B C → A ∈ X → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
63 3 62 sylbi ⊢ V = A ∨ V = A B ∨ V = A B C → A ∈ X → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E
64 63 impcom ⊢ A ∈ X ∧ V = A ∨ V = A B ∨ V = A B C → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E