Metamath Proof Explorer

Theorem 3vfriswmgr

Description: Every friendship graph with three (different) 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 3vfriswmgr ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧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 frgrusgr ⊢G∈FriendGraph→G∈USGraph
4 1 2 frgr3v ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C→V=ABC∧G∈USGraph→G∈FriendGraph↔AB∈E∧BC∈E∧CA∈E
5 4 exp4b ⊢A∈X∧B∈Y∧C∈Z→A≠B∧A≠C∧B≠C→V=ABC→G∈USGraph→G∈FriendGraph↔AB∈E∧BC∈E∧CA∈E
6 5 3imp1 ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→G∈FriendGraph↔AB∈E∧BC∈E∧CA∈E
7 prcom ⊢CA=AC
8 7 eleq1i ⊢CA∈E↔AC∈E
9 8 biimpi ⊢CA∈E→AC∈E
10 9 3ad2ant3 ⊢AB∈E∧BC∈E∧CA∈E→AC∈E
11 10 adantl ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph∧AB∈E∧BC∈E∧CA∈E→AC∈E
12 simpl11 ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→A∈X
13 simpl12 ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→B∈Y
14 simp1 ⊢A≠B∧A≠C∧B≠C→A≠B
15 14 3ad2ant2 ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC→A≠B
16 15 adantr ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→A≠B
17 12 13 16 3jca ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→A∈X∧B∈Y∧A≠B
18 simp3 ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC→V=ABC
19 18 anim1i ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→V=ABC∧G∈USGraph
20 17 19 jca ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→A∈X∧B∈Y∧A≠B∧V=ABC∧G∈USGraph
21 simp1 ⊢AB∈E∧BC∈E∧CA∈E→AB∈E
22 1 2 3vfriswmgrlem ⊢A∈X∧B∈Y∧A≠B∧V=ABC∧G∈USGraph→AB∈E→∃!w∈ABAw∈E
23 22 imp ⊢A∈X∧B∈Y∧A≠B∧V=ABC∧G∈USGraph∧AB∈E→∃!w∈ABAw∈E
24 20 21 23 syl2an ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph∧AB∈E∧BC∈E∧CA∈E→∃!w∈ABAw∈E
25 11 24 jca ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph∧AB∈E∧BC∈E∧CA∈E→AC∈E∧∃!w∈ABAw∈E
26 simpr2 ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph∧AB∈E∧BC∈E∧CA∈E→BC∈E
27 necom ⊢A≠B↔B≠A
28 27 biimpi ⊢A≠B→B≠A
29 28 3ad2ant1 ⊢A≠B∧A≠C∧B≠C→B≠A
30 29 3ad2ant2 ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC→B≠A
31 30 adantr ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→B≠A
32 13 12 31 3jca ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→B∈Y∧A∈X∧B≠A
33 tpcoma ⊢ABC=BAC
34 18 33 eqtrdi ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC→V=BAC
35 34 anim1i ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→V=BAC∧G∈USGraph
36 32 35 jca ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→B∈Y∧A∈X∧B≠A∧V=BAC∧G∈USGraph
37 prcom ⊢AB=BA
38 37 eleq1i ⊢AB∈E↔BA∈E
39 38 biimpi ⊢AB∈E→BA∈E
40 39 3ad2ant1 ⊢AB∈E∧BC∈E∧CA∈E→BA∈E
41 1 2 3vfriswmgrlem ⊢B∈Y∧A∈X∧B≠A∧V=BAC∧G∈USGraph→BA∈E→∃!w∈BABw∈E
42 41 imp ⊢B∈Y∧A∈X∧B≠A∧V=BAC∧G∈USGraph∧BA∈E→∃!w∈BABw∈E
43 reueq1 ⊢AB=BA→∃!w∈ABBw∈E↔∃!w∈BABw∈E
44 37 43 ax-mp ⊢∃!w∈ABBw∈E↔∃!w∈BABw∈E
45 42 44 sylibr ⊢B∈Y∧A∈X∧B≠A∧V=BAC∧G∈USGraph∧BA∈E→∃!w∈ABBw∈E
46 36 40 45 syl2an ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph∧AB∈E∧BC∈E∧CA∈E→∃!w∈ABBw∈E
47 26 46 jca ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph∧AB∈E∧BC∈E∧CA∈E→BC∈E∧∃!w∈ABBw∈E
48 25 47 jca ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph∧AB∈E∧BC∈E∧CA∈E→AC∈E∧∃!w∈ABAw∈E∧BC∈E∧∃!w∈ABBw∈E
49 preq1 ⊢v=A→vC=AC
50 49 eleq1d ⊢v=A→vC∈E↔AC∈E
51 preq1 ⊢v=A→vw=Aw
52 51 eleq1d ⊢v=A→vw∈E↔Aw∈E
53 52 reubidv ⊢v=A→∃!w∈ABvw∈E↔∃!w∈ABAw∈E
54 50 53 anbi12d ⊢v=A→vC∈E∧∃!w∈ABvw∈E↔AC∈E∧∃!w∈ABAw∈E
55 preq1 ⊢v=B→vC=BC
56 55 eleq1d ⊢v=B→vC∈E↔BC∈E
57 preq1 ⊢v=B→vw=Bw
58 57 eleq1d ⊢v=B→vw∈E↔Bw∈E
59 58 reubidv ⊢v=B→∃!w∈ABvw∈E↔∃!w∈ABBw∈E
60 56 59 anbi12d ⊢v=B→vC∈E∧∃!w∈ABvw∈E↔BC∈E∧∃!w∈ABBw∈E
61 54 60 ralprg ⊢A∈X∧B∈Y→∀v∈ABvC∈E∧∃!w∈ABvw∈E↔AC∈E∧∃!w∈ABAw∈E∧BC∈E∧∃!w∈ABBw∈E
62 61 3adant3 ⊢A∈X∧B∈Y∧C∈Z→∀v∈ABvC∈E∧∃!w∈ABvw∈E↔AC∈E∧∃!w∈ABAw∈E∧BC∈E∧∃!w∈ABBw∈E
63 62 3ad2ant1 ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC→∀v∈ABvC∈E∧∃!w∈ABvw∈E↔AC∈E∧∃!w∈ABAw∈E∧BC∈E∧∃!w∈ABBw∈E
64 63 adantr ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→∀v∈ABvC∈E∧∃!w∈ABvw∈E↔AC∈E∧∃!w∈ABAw∈E∧BC∈E∧∃!w∈ABBw∈E
65 64 adantr ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph∧AB∈E∧BC∈E∧CA∈E→∀v∈ABvC∈E∧∃!w∈ABvw∈E↔AC∈E∧∃!w∈ABAw∈E∧BC∈E∧∃!w∈ABBw∈E
66 48 65 mpbird ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph∧AB∈E∧BC∈E∧CA∈E→∀v∈ABvC∈E∧∃!w∈ABvw∈E
67 diftpsn3 ⊢A≠C∧B≠C→ABC∖C=AB
68 67 3adant1 ⊢A≠B∧A≠C∧B≠C→ABC∖C=AB
69 reueq1 ⊢ABC∖C=AB→∃!w∈ABC∖Cvw∈E↔∃!w∈ABvw∈E
70 68 69 syl ⊢A≠B∧A≠C∧B≠C→∃!w∈ABC∖Cvw∈E↔∃!w∈ABvw∈E
71 70 anbi2d ⊢A≠B∧A≠C∧B≠C→vC∈E∧∃!w∈ABC∖Cvw∈E↔vC∈E∧∃!w∈ABvw∈E
72 68 71 raleqbidv ⊢A≠B∧A≠C∧B≠C→∀v∈ABC∖CvC∈E∧∃!w∈ABC∖Cvw∈E↔∀v∈ABvC∈E∧∃!w∈ABvw∈E
73 72 3ad2ant2 ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC→∀v∈ABC∖CvC∈E∧∃!w∈ABC∖Cvw∈E↔∀v∈ABvC∈E∧∃!w∈ABvw∈E
74 73 adantr ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→∀v∈ABC∖CvC∈E∧∃!w∈ABC∖Cvw∈E↔∀v∈ABvC∈E∧∃!w∈ABvw∈E
75 74 adantr ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph∧AB∈E∧BC∈E∧CA∈E→∀v∈ABC∖CvC∈E∧∃!w∈ABC∖Cvw∈E↔∀v∈ABvC∈E∧∃!w∈ABvw∈E
76 66 75 mpbird ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph∧AB∈E∧BC∈E∧CA∈E→∀v∈ABC∖CvC∈E∧∃!w∈ABC∖Cvw∈E
77 76 3mix3d ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph∧AB∈E∧BC∈E∧CA∈E→∀v∈ABC∖AvA∈E∧∃!w∈ABC∖Avw∈E∨∀v∈ABC∖BvB∈E∧∃!w∈ABC∖Bvw∈E∨∀v∈ABC∖CvC∈E∧∃!w∈ABC∖Cvw∈E
78 sneq ⊢h=A→h=A
79 78 difeq2d ⊢h=A→ABC∖h=ABC∖A
80 preq2 ⊢h=A→vh=vA
81 80 eleq1d ⊢h=A→vh∈E↔vA∈E
82 reueq1 ⊢ABC∖h=ABC∖A→∃!w∈ABC∖hvw∈E↔∃!w∈ABC∖Avw∈E
83 79 82 syl ⊢h=A→∃!w∈ABC∖hvw∈E↔∃!w∈ABC∖Avw∈E
84 81 83 anbi12d ⊢h=A→vh∈E∧∃!w∈ABC∖hvw∈E↔vA∈E∧∃!w∈ABC∖Avw∈E
85 79 84 raleqbidv ⊢h=A→∀v∈ABC∖hvh∈E∧∃!w∈ABC∖hvw∈E↔∀v∈ABC∖AvA∈E∧∃!w∈ABC∖Avw∈E
86 sneq ⊢h=B→h=B
87 86 difeq2d ⊢h=B→ABC∖h=ABC∖B
88 preq2 ⊢h=B→vh=vB
89 88 eleq1d ⊢h=B→vh∈E↔vB∈E
90 reueq1 ⊢ABC∖h=ABC∖B→∃!w∈ABC∖hvw∈E↔∃!w∈ABC∖Bvw∈E
91 87 90 syl ⊢h=B→∃!w∈ABC∖hvw∈E↔∃!w∈ABC∖Bvw∈E
92 89 91 anbi12d ⊢h=B→vh∈E∧∃!w∈ABC∖hvw∈E↔vB∈E∧∃!w∈ABC∖Bvw∈E
93 87 92 raleqbidv ⊢h=B→∀v∈ABC∖hvh∈E∧∃!w∈ABC∖hvw∈E↔∀v∈ABC∖BvB∈E∧∃!w∈ABC∖Bvw∈E
94 sneq ⊢h=C→h=C
95 94 difeq2d ⊢h=C→ABC∖h=ABC∖C
96 preq2 ⊢h=C→vh=vC
97 96 eleq1d ⊢h=C→vh∈E↔vC∈E
98 reueq1 ⊢ABC∖h=ABC∖C→∃!w∈ABC∖hvw∈E↔∃!w∈ABC∖Cvw∈E
99 95 98 syl ⊢h=C→∃!w∈ABC∖hvw∈E↔∃!w∈ABC∖Cvw∈E
100 97 99 anbi12d ⊢h=C→vh∈E∧∃!w∈ABC∖hvw∈E↔vC∈E∧∃!w∈ABC∖Cvw∈E
101 95 100 raleqbidv ⊢h=C→∀v∈ABC∖hvh∈E∧∃!w∈ABC∖hvw∈E↔∀v∈ABC∖CvC∈E∧∃!w∈ABC∖Cvw∈E
102 85 93 101 rextpg ⊢A∈X∧B∈Y∧C∈Z→∃h∈ABC∀v∈ABC∖hvh∈E∧∃!w∈ABC∖hvw∈E↔∀v∈ABC∖AvA∈E∧∃!w∈ABC∖Avw∈E∨∀v∈ABC∖BvB∈E∧∃!w∈ABC∖Bvw∈E∨∀v∈ABC∖CvC∈E∧∃!w∈ABC∖Cvw∈E
103 102 3ad2ant1 ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC→∃h∈ABC∀v∈ABC∖hvh∈E∧∃!w∈ABC∖hvw∈E↔∀v∈ABC∖AvA∈E∧∃!w∈ABC∖Avw∈E∨∀v∈ABC∖BvB∈E∧∃!w∈ABC∖Bvw∈E∨∀v∈ABC∖CvC∈E∧∃!w∈ABC∖Cvw∈E
104 103 adantr ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→∃h∈ABC∀v∈ABC∖hvh∈E∧∃!w∈ABC∖hvw∈E↔∀v∈ABC∖AvA∈E∧∃!w∈ABC∖Avw∈E∨∀v∈ABC∖BvB∈E∧∃!w∈ABC∖Bvw∈E∨∀v∈ABC∖CvC∈E∧∃!w∈ABC∖Cvw∈E
105 104 adantr ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph∧AB∈E∧BC∈E∧CA∈E→∃h∈ABC∀v∈ABC∖hvh∈E∧∃!w∈ABC∖hvw∈E↔∀v∈ABC∖AvA∈E∧∃!w∈ABC∖Avw∈E∨∀v∈ABC∖BvB∈E∧∃!w∈ABC∖Bvw∈E∨∀v∈ABC∖CvC∈E∧∃!w∈ABC∖Cvw∈E
106 77 105 mpbird ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph∧AB∈E∧BC∈E∧CA∈E→∃h∈ABC∀v∈ABC∖hvh∈E∧∃!w∈ABC∖hvw∈E
107 106 ex ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→AB∈E∧BC∈E∧CA∈E→∃h∈ABC∀v∈ABC∖hvh∈E∧∃!w∈ABC∖hvw∈E
108 6 107 sylbid ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→G∈FriendGraph→∃h∈ABC∀v∈ABC∖hvh∈E∧∃!w∈ABC∖hvw∈E
109 108 expcom ⊢G∈USGraph→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC→G∈FriendGraph→∃h∈ABC∀v∈ABC∖hvh∈E∧∃!w∈ABC∖hvw∈E
110 109 com23 ⊢G∈USGraph→G∈FriendGraph→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC→∃h∈ABC∀v∈ABC∖hvh∈E∧∃!w∈ABC∖hvw∈E
111 3 110 mpcom ⊢G∈FriendGraph→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC→∃h∈ABC∀v∈ABC∖hvh∈E∧∃!w∈ABC∖hvw∈E
112 111 com12 ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC→G∈FriendGraph→∃h∈ABC∀v∈ABC∖hvh∈E∧∃!w∈ABC∖hvw∈E
113 difeq1 ⊢V=ABC→V∖h=ABC∖h
114 reueq1 ⊢V∖h=ABC∖h→∃!w∈V∖hvw∈E↔∃!w∈ABC∖hvw∈E
115 113 114 syl ⊢V=ABC→∃!w∈V∖hvw∈E↔∃!w∈ABC∖hvw∈E
116 115 anbi2d ⊢V=ABC→vh∈E∧∃!w∈V∖hvw∈E↔vh∈E∧∃!w∈ABC∖hvw∈E
117 113 116 raleqbidv ⊢V=ABC→∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E↔∀v∈ABC∖hvh∈E∧∃!w∈ABC∖hvw∈E
118 117 rexeqbi1dv ⊢V=ABC→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E↔∃h∈ABC∀v∈ABC∖hvh∈E∧∃!w∈ABC∖hvw∈E
119 118 imbi2d ⊢V=ABC→G∈FriendGraph→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E↔G∈FriendGraph→∃h∈ABC∀v∈ABC∖hvh∈E∧∃!w∈ABC∖hvw∈E
120 119 3ad2ant3 ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC→G∈FriendGraph→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E↔G∈FriendGraph→∃h∈ABC∀v∈ABC∖hvh∈E∧∃!w∈ABC∖hvw∈E
121 112 120 mpbird ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC→G∈FriendGraph→∃h∈V∀v∈V∖hvh∈E∧∃!w∈V∖hvw∈E