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=AB∨V=ABC→G∈FriendGraph→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E

Proof

Step Hyp Ref Expression
1 3vfriswmgr.v ⊢V=Vtx⁡G
2 3vfriswmgr.e ⊢E=Edg⁡G
3 df-3or ⊢V=A∨V=AB∨V=ABC↔V=A∨V=AB∨V=ABC
4 1 2 1to2vfriswmgr ⊢A∈X∧V=A∨V=AB→G∈FriendGraph→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E
5 4 expcom ⊢V=A∨V=AB→A∈X→G∈FriendGraph→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E
6 tppreq3 ⊢B=C→ABC=AB
7 6 eqeq2d ⊢B=C→V=ABC↔V=AB
8 olc ⊢V=AB→V=A∨V=AB
9 8 anim1ci ⊢V=AB∧A∈X→A∈X∧V=A∨V=AB
10 9 4 syl ⊢V=AB∧A∈X→G∈FriendGraph→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E
11 10 ex ⊢V=AB→A∈X→G∈FriendGraph→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E
12 7 11 syl6bi ⊢B=C→V=ABC→A∈X→G∈FriendGraph→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E
13 tpprceq3 ⊢¬B∈V∧B≠A→CAB=CA
14 tprot ⊢CAB=ABC
15 14 eqeq1i ⊢CAB=CA↔ABC=CA
16 15 biimpi ⊢CAB=CA→ABC=CA
17 prcom ⊢CA=AC
18 16 17 eqtrdi ⊢CAB=CA→ABC=AC
19 18 eqeq2d ⊢CAB=CA→V=ABC↔V=AC
20 olc ⊢V=AC→V=A∨V=AC
21 1 2 1to2vfriswmgr ⊢A∈X∧V=A∨V=AC→G∈FriendGraph→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E
22 20 21 sylan2 ⊢A∈X∧V=AC→G∈FriendGraph→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E
23 22 expcom ⊢V=AC→A∈X→G∈FriendGraph→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E
24 19 23 syl6bi ⊢CAB=CA→V=ABC→A∈X→G∈FriendGraph→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E
25 13 24 syl ⊢¬B∈V∧B≠A→V=ABC→A∈X→G∈FriendGraph→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E
26 25 a1d ⊢¬B∈V∧B≠A→B≠C→V=ABC→A∈X→G∈FriendGraph→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E
27 tpprceq3 ⊢¬C∈V∧C≠A→BAC=BA
28 tpcoma ⊢BAC=ABC
29 28 eqeq1i ⊢BAC=BA↔ABC=BA
30 29 biimpi ⊢BAC=BA→ABC=BA
31 prcom ⊢BA=AB
32 30 31 eqtrdi ⊢BAC=BA→ABC=AB
33 32 eqeq2d ⊢BAC=BA→V=ABC↔V=AB
34 8 4 sylan2 ⊢A∈X∧V=AB→G∈FriendGraph→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E
35 34 expcom ⊢V=AB→A∈X→G∈FriendGraph→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E
36 35 a1d ⊢V=AB→B≠C→A∈X→G∈FriendGraph→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E
37 33 36 syl6bi ⊢BAC=BA→V=ABC→B≠C→A∈X→G∈FriendGraph→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E
38 27 37 syl ⊢¬C∈V∧C≠A→V=ABC→B≠C→A∈X→G∈FriendGraph→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E
39 38 com23 ⊢¬C∈V∧C≠A→B≠C→V=ABC→A∈X→G∈FriendGraph→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈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=ABC→B∈V∧C∈V
44 43 anim1ci ⊢B∈V∧B≠A∧C∈V∧C≠A∧B≠C∧V=ABC∧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=ABC∧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=ABC∧A∈X→A≠B∧A≠C∧B≠C
56 simplr ⊢B∈V∧B≠A∧C∈V∧C≠A∧B≠C∧V=ABC∧A∈X→V=ABC
57 1 2 3vfriswmgr ⊢A∈X∧B∈V∧C∈V∧A≠B∧A≠C∧B≠C∧V=ABC→G∈FriendGraph→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E
58 46 55 56 57 syl3anc ⊢B∈V∧B≠A∧C∈V∧C≠A∧B≠C∧V=ABC∧A∈X→G∈FriendGraph→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E
59 58 exp41 ⊢B∈V∧B≠A∧C∈V∧C≠A→B≠C→V=ABC→A∈X→G∈FriendGraph→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E
60 26 39 59 ecase ⊢B≠C→V=ABC→A∈X→G∈FriendGraph→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E
61 12 60 pm2.61ine ⊢V=ABC→A∈X→G∈FriendGraph→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E
62 5 61 jaoi ⊢V=A∨V=AB∨V=ABC→A∈X→G∈FriendGraph→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E
63 3 62 sylbi ⊢V=A∨V=AB∨V=ABC→A∈X→G∈FriendGraph→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E
64 63 impcom ⊢A∈X∧V=A∨V=AB∨V=ABC→G∈FriendGraph→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E