Metamath Proof Explorer


Theorem frgr3v

Description: Any graph with three vertices which are completely connected with each other is a friendship graph. (Contributed by Alexander van der Vekens, 5-Oct-2017) (Revised by AV, 29-Mar-2021)

Ref Expression
Hypotheses frgr3v.v V = Vtx G
frgr3v.e E = Edg G
Assertion frgr3v A X B Y C Z A B A C B C V = A B C G USGraph G FriendGraph A B E B C E C A E

Proof

Step Hyp Ref Expression
1 frgr3v.v V = Vtx G
2 frgr3v.e E = Edg G
3 1 2 isfrgr G FriendGraph G USGraph k V l V k ∃! x V x k x l E
4 3 a1i A X B Y C Z A B A C B C V = A B C G USGraph G FriendGraph G USGraph k V l V k ∃! x V x k x l E
5 id V = A B C V = A B C
6 difeq1 V = A B C V k = A B C k
7 reueq1 V = A B C ∃! x V x k x l E ∃! x A B C x k x l E
8 6 7 raleqbidv V = A B C l V k ∃! x V x k x l E l A B C k ∃! x A B C x k x l E
9 5 8 raleqbidv V = A B C k V l V k ∃! x V x k x l E k A B C l A B C k ∃! x A B C x k x l E
10 9 anbi2d V = A B C G USGraph k V l V k ∃! x V x k x l E G USGraph k A B C l A B C k ∃! x A B C x k x l E
11 10 baibd V = A B C G USGraph G USGraph k V l V k ∃! x V x k x l E k A B C l A B C k ∃! x A B C x k x l E
12 11 adantl A X B Y C Z A B A C B C V = A B C G USGraph G USGraph k V l V k ∃! x V x k x l E k A B C l A B C k ∃! x A B C x k x l E
13 4 12 bitrd A X B Y C Z A B A C B C V = A B C G USGraph G FriendGraph k A B C l A B C k ∃! x A B C x k x l E
14 sneq k = A k = A
15 14 difeq2d k = A A B C k = A B C A
16 preq2 k = A x k = x A
17 16 preq1d k = A x k x l = x A x l
18 17 sseq1d k = A x k x l E x A x l E
19 18 reubidv k = A ∃! x A B C x k x l E ∃! x A B C x A x l E
20 15 19 raleqbidv k = A l A B C k ∃! x A B C x k x l E l A B C A ∃! x A B C x A x l E
21 sneq k = B k = B
22 21 difeq2d k = B A B C k = A B C B
23 preq2 k = B x k = x B
24 23 preq1d k = B x k x l = x B x l
25 24 sseq1d k = B x k x l E x B x l E
26 25 reubidv k = B ∃! x A B C x k x l E ∃! x A B C x B x l E
27 22 26 raleqbidv k = B l A B C k ∃! x A B C x k x l E l A B C B ∃! x A B C x B x l E
28 sneq k = C k = C
29 28 difeq2d k = C A B C k = A B C C
30 preq2 k = C x k = x C
31 30 preq1d k = C x k x l = x C x l
32 31 sseq1d k = C x k x l E x C x l E
33 32 reubidv k = C ∃! x A B C x k x l E ∃! x A B C x C x l E
34 29 33 raleqbidv k = C l A B C k ∃! x A B C x k x l E l A B C C ∃! x A B C x C x l E
35 20 27 34 raltpg A X B Y C Z k A B C l A B C k ∃! x A B C x k x l E l A B C A ∃! x A B C x A x l E l A B C B ∃! x A B C x B x l E l A B C C ∃! x A B C x C x l E
36 35 ad2antrr A X B Y C Z A B A C B C V = A B C G USGraph k A B C l A B C k ∃! x A B C x k x l E l A B C A ∃! x A B C x A x l E l A B C B ∃! x A B C x B x l E l A B C C ∃! x A B C x C x l E
37 tprot A B C = B C A
38 37 a1i A B A C B C A B C = B C A
39 38 difeq1d A B A C B C A B C A = B C A A
40 necom A B B A
41 40 biimpi A B B A
42 necom A C C A
43 42 biimpi A C C A
44 41 43 anim12i A B A C B A C A
45 44 3adant3 A B A C B C B A C A
46 diftpsn3 B A C A B C A A = B C
47 45 46 syl A B A C B C B C A A = B C
48 39 47 eqtrd A B A C B C A B C A = B C
49 48 raleqdv A B A C B C l A B C A ∃! x A B C x A x l E l B C ∃! x A B C x A x l E
50 tprot C A B = A B C
51 50 eqcomi A B C = C A B
52 51 a1i A B A C B C A B C = C A B
53 52 difeq1d A B A C B C A B C B = C A B B
54 id A B A B
55 necom B C C B
56 55 biimpi B C C B
57 54 56 anim12ci A B B C C B A B
58 57 3adant2 A B A C B C C B A B
59 diftpsn3 C B A B C A B B = C A
60 58 59 syl A B A C B C C A B B = C A
61 53 60 eqtrd A B A C B C A B C B = C A
62 61 raleqdv A B A C B C l A B C B ∃! x A B C x B x l E l C A ∃! x A B C x B x l E
63 diftpsn3 A C B C A B C C = A B
64 63 3adant1 A B A C B C A B C C = A B
65 64 raleqdv A B A C B C l A B C C ∃! x A B C x C x l E l A B ∃! x A B C x C x l E
66 49 62 65 3anbi123d A B A C B C l A B C A ∃! x A B C x A x l E l A B C B ∃! x A B C x B x l E l A B C C ∃! x A B C x C x l E l B C ∃! x A B C x A x l E l C A ∃! x A B C x B x l E l A B ∃! x A B C x C x l E
67 66 ad2antlr A X B Y C Z A B A C B C V = A B C G USGraph l A B C A ∃! x A B C x A x l E l A B C B ∃! x A B C x B x l E l A B C C ∃! x A B C x C x l E l B C ∃! x A B C x A x l E l C A ∃! x A B C x B x l E l A B ∃! x A B C x C x l E
68 preq2 l = B x l = x B
69 68 preq2d l = B x A x l = x A x B
70 69 sseq1d l = B x A x l E x A x B E
71 70 reubidv l = B ∃! x A B C x A x l E ∃! x A B C x A x B E
72 preq2 l = C x l = x C
73 72 preq2d l = C x A x l = x A x C
74 73 sseq1d l = C x A x l E x A x C E
75 74 reubidv l = C ∃! x A B C x A x l E ∃! x A B C x A x C E
76 71 75 ralprg B Y C Z l B C ∃! x A B C x A x l E ∃! x A B C x A x B E ∃! x A B C x A x C E
77 76 3adant1 A X B Y C Z l B C ∃! x A B C x A x l E ∃! x A B C x A x B E ∃! x A B C x A x C E
78 72 preq2d l = C x B x l = x B x C
79 78 sseq1d l = C x B x l E x B x C E
80 79 reubidv l = C ∃! x A B C x B x l E ∃! x A B C x B x C E
81 preq2 l = A x l = x A
82 81 preq2d l = A x B x l = x B x A
83 82 sseq1d l = A x B x l E x B x A E
84 83 reubidv l = A ∃! x A B C x B x l E ∃! x A B C x B x A E
85 80 84 ralprg C Z A X l C A ∃! x A B C x B x l E ∃! x A B C x B x C E ∃! x A B C x B x A E
86 85 ancoms A X C Z l C A ∃! x A B C x B x l E ∃! x A B C x B x C E ∃! x A B C x B x A E
87 86 3adant2 A X B Y C Z l C A ∃! x A B C x B x l E ∃! x A B C x B x C E ∃! x A B C x B x A E
88 81 preq2d l = A x C x l = x C x A
89 88 sseq1d l = A x C x l E x C x A E
90 89 reubidv l = A ∃! x A B C x C x l E ∃! x A B C x C x A E
91 68 preq2d l = B x C x l = x C x B
92 91 sseq1d l = B x C x l E x C x B E
93 92 reubidv l = B ∃! x A B C x C x l E ∃! x A B C x C x B E
94 90 93 ralprg A X B Y l A B ∃! x A B C x C x l E ∃! x A B C x C x A E ∃! x A B C x C x B E
95 94 3adant3 A X B Y C Z l A B ∃! x A B C x C x l E ∃! x A B C x C x A E ∃! x A B C x C x B E
96 77 87 95 3anbi123d A X B Y C Z l B C ∃! x A B C x A x l E l C A ∃! x A B C x B x l E l A B ∃! x A B C x C x l E ∃! x A B C x A x B E ∃! x A B C x A x C E ∃! x A B C x B x C E ∃! x A B C x B x A E ∃! x A B C x C x A E ∃! x A B C x C x B E
97 96 ad2antrr A X B Y C Z A B A C B C V = A B C G USGraph l B C ∃! x A B C x A x l E l C A ∃! x A B C x B x l E l A B ∃! x A B C x C x l E ∃! x A B C x A x B E ∃! x A B C x A x C E ∃! x A B C x B x C E ∃! x A B C x B x A E ∃! x A B C x C x A E ∃! x A B C x C x B E
98 36 67 97 3bitrd A X B Y C Z A B A C B C V = A B C G USGraph k A B C l A B C k ∃! x A B C x k x l E ∃! x A B C x A x B E ∃! x A B C x A x C E ∃! x A B C x B x C E ∃! x A B C x B x A E ∃! x A B C x C x A E ∃! x A B C x C x B E
99 1 2 frgr3vlem2 A X B Y C Z A B A C B C V = A B C G USGraph ∃! x A B C x A x B E C A E C B E
100 99 imp A X B Y C Z A B A C B C V = A B C G USGraph ∃! x A B C x A x B E C A E C B E
101 simpll1 A X B Y C Z A B A C B C V = A B C G USGraph A X
102 simpll3 A X B Y C Z A B A C B C V = A B C G USGraph C Z
103 simpll2 A X B Y C Z A B A C B C V = A B C G USGraph B Y
104 101 102 103 3jca A X B Y C Z A B A C B C V = A B C G USGraph A X C Z B Y
105 simplr2 A X B Y C Z A B A C B C V = A B C G USGraph A C
106 simplr1 A X B Y C Z A B A C B C V = A B C G USGraph A B
107 58 simpld A B A C B C C B
108 107 ad2antlr A X B Y C Z A B A C B C V = A B C G USGraph C B
109 105 106 108 3jca A X B Y C Z A B A C B C V = A B C G USGraph A C A B C B
110 tpcomb A B C = A C B
111 5 110 eqtrdi V = A B C V = A C B
112 111 anim1i V = A B C G USGraph V = A C B G USGraph
113 112 adantl A X B Y C Z A B A C B C V = A B C G USGraph V = A C B G USGraph
114 reueq1 A B C = A C B ∃! x A B C x A x C E ∃! x A C B x A x C E
115 110 114 mp1i A X C Z B Y A C A B C B V = A C B G USGraph ∃! x A B C x A x C E ∃! x A C B x A x C E
116 1 2 frgr3vlem2 A X C Z B Y A C A B C B V = A C B G USGraph ∃! x A C B x A x C E B A E B C E
117 116 imp A X C Z B Y A C A B C B V = A C B G USGraph ∃! x A C B x A x C E B A E B C E
118 115 117 bitrd A X C Z B Y A C A B C B V = A C B G USGraph ∃! x A B C x A x C E B A E B C E
119 104 109 113 118 syl21anc A X B Y C Z A B A C B C V = A B C G USGraph ∃! x A B C x A x C E B A E B C E
120 100 119 anbi12d A X B Y C Z A B A C B C V = A B C G USGraph ∃! x A B C x A x B E ∃! x A B C x A x C E C A E C B E B A E B C E
121 103 102 101 3jca A X B Y C Z A B A C B C V = A B C G USGraph B Y C Z A X
122 simplr3 A X B Y C Z A B A C B C V = A B C G USGraph B C
123 106 necomd A X B Y C Z A B A C B C V = A B C G USGraph B A
124 105 necomd A X B Y C Z A B A C B C V = A B C G USGraph C A
125 122 123 124 3jca A X B Y C Z A B A C B C V = A B C G USGraph B C B A C A
126 37 eqeq2i V = A B C V = B C A
127 126 biimpi V = A B C V = B C A
128 127 anim1i V = A B C G USGraph V = B C A G USGraph
129 128 adantl A X B Y C Z A B A C B C V = A B C G USGraph V = B C A G USGraph
130 reueq1 A B C = B C A ∃! x A B C x B x C E ∃! x B C A x B x C E
131 37 130 mp1i B Y C Z A X B C B A C A V = B C A G USGraph ∃! x A B C x B x C E ∃! x B C A x B x C E
132 1 2 frgr3vlem2 B Y C Z A X B C B A C A V = B C A G USGraph ∃! x B C A x B x C E A B E A C E
133 132 imp B Y C Z A X B C B A C A V = B C A G USGraph ∃! x B C A x B x C E A B E A C E
134 131 133 bitrd B Y C Z A X B C B A C A V = B C A G USGraph ∃! x A B C x B x C E A B E A C E
135 121 125 129 134 syl21anc A X B Y C Z A B A C B C V = A B C G USGraph ∃! x A B C x B x C E A B E A C E
136 103 101 102 3jca A X B Y C Z A B A C B C V = A B C G USGraph B Y A X C Z
137 123 122 105 3jca A X B Y C Z A B A C B C V = A B C G USGraph B A B C A C
138 tpcoma A B C = B A C
139 138 eqeq2i V = A B C V = B A C
140 139 biimpi V = A B C V = B A C
141 140 anim1i V = A B C G USGraph V = B A C G USGraph
142 141 adantl A X B Y C Z A B A C B C V = A B C G USGraph V = B A C G USGraph
143 reueq1 A B C = B A C ∃! x A B C x B x A E ∃! x B A C x B x A E
144 138 143 mp1i B Y A X C Z B A B C A C V = B A C G USGraph ∃! x A B C x B x A E ∃! x B A C x B x A E
145 1 2 frgr3vlem2 B Y A X C Z B A B C A C V = B A C G USGraph ∃! x B A C x B x A E C B E C A E
146 145 imp B Y A X C Z B A B C A C V = B A C G USGraph ∃! x B A C x B x A E C B E C A E
147 144 146 bitrd B Y A X C Z B A B C A C V = B A C G USGraph ∃! x A B C x B x A E C B E C A E
148 136 137 142 147 syl21anc A X B Y C Z A B A C B C V = A B C G USGraph ∃! x A B C x B x A E C B E C A E
149 135 148 anbi12d A X B Y C Z A B A C B C V = A B C G USGraph ∃! x A B C x B x C E ∃! x A B C x B x A E A B E A C E C B E C A E
150 102 101 103 3jca A X B Y C Z A B A C B C V = A B C G USGraph C Z A X B Y
151 124 108 106 3jca A X B Y C Z A B A C B C V = A B C G USGraph C A C B A B
152 51 eqeq2i V = A B C V = C A B
153 152 biimpi V = A B C V = C A B
154 153 anim1i V = A B C G USGraph V = C A B G USGraph
155 154 adantl A X B Y C Z A B A C B C V = A B C G USGraph V = C A B G USGraph
156 reueq1 A B C = C A B ∃! x A B C x C x A E ∃! x C A B x C x A E
157 51 156 mp1i C Z A X B Y C A C B A B V = C A B G USGraph ∃! x A B C x C x A E ∃! x C A B x C x A E
158 1 2 frgr3vlem2 C Z A X B Y C A C B A B V = C A B G USGraph ∃! x C A B x C x A E B C E B A E
159 158 imp C Z A X B Y C A C B A B V = C A B G USGraph ∃! x C A B x C x A E B C E B A E
160 157 159 bitrd C Z A X B Y C A C B A B V = C A B G USGraph ∃! x A B C x C x A E B C E B A E
161 150 151 155 160 syl21anc A X B Y C Z A B A C B C V = A B C G USGraph ∃! x A B C x C x A E B C E B A E
162 3anrev A X B Y C Z C Z B Y A X
163 162 biimpi A X B Y C Z C Z B Y A X
164 55 42 40 3anbi123i B C A C A B C B C A B A
165 164 biimpi B C A C A B C B C A B A
166 165 3com13 A B A C B C C B C A B A
167 163 166 anim12i A X B Y C Z A B A C B C C Z B Y A X C B C A B A
168 tpcoma B C A = C B A
169 37 168 eqtri A B C = C B A
170 169 eqeq2i V = A B C V = C B A
171 170 biimpi V = A B C V = C B A
172 171 anim1i V = A B C G USGraph V = C B A G USGraph
173 reueq1 A B C = C B A ∃! x A B C x C x B E ∃! x C B A x C x B E
174 169 173 mp1i C Z B Y A X C B C A B A V = C B A G USGraph ∃! x A B C x C x B E ∃! x C B A x C x B E
175 1 2 frgr3vlem2 C Z B Y A X C B C A B A V = C B A G USGraph ∃! x C B A x C x B E A C E A B E
176 175 imp C Z B Y A X C B C A B A V = C B A G USGraph ∃! x C B A x C x B E A C E A B E
177 174 176 bitrd C Z B Y A X C B C A B A V = C B A G USGraph ∃! x A B C x C x B E A C E A B E
178 167 172 177 syl2an A X B Y C Z A B A C B C V = A B C G USGraph ∃! x A B C x C x B E A C E A B E
179 161 178 anbi12d A X B Y C Z A B A C B C V = A B C G USGraph ∃! x A B C x C x A E ∃! x A B C x C x B E B C E B A E A C E A B E
180 120 149 179 3anbi123d A X B Y C Z A B A C B C V = A B C G USGraph ∃! x A B C x A x B E ∃! x A B C x A x C E ∃! x A B C x B x C E ∃! x A B C x B x A E ∃! x A B C x C x A E ∃! x A B C x C x B E C A E C B E B A E B C E A B E A C E C B E C A E B C E B A E A C E A B E
181 prcom B C = C B
182 181 eleq1i B C E C B E
183 182 anbi2i B A E B C E B A E C B E
184 183 anbi2i C A E C B E B A E B C E C A E C B E B A E C B E
185 anandir C A E B A E C B E C A E C B E B A E C B E
186 184 185 bitr4i C A E C B E B A E B C E C A E B A E C B E
187 prcom C A = A C
188 187 eleq1i C A E A C E
189 188 anbi2i C B E C A E C B E A C E
190 189 anbi2i A B E A C E C B E C A E A B E A C E C B E A C E
191 anandir A B E C B E A C E A B E A C E C B E A C E
192 190 191 bitr4i A B E A C E C B E C A E A B E C B E A C E
193 prcom A B = B A
194 193 eleq1i A B E B A E
195 194 anbi2i A C E A B E A C E B A E
196 195 anbi2i B C E B A E A C E A B E B C E B A E A C E B A E
197 anandir B C E A C E B A E B C E B A E A C E B A E
198 196 197 bitr4i B C E B A E A C E A B E B C E A C E B A E
199 186 192 198 3anbi123i C A E C B E B A E B C E A B E A C E C B E C A E B C E B A E A C E A B E C A E B A E C B E A B E C B E A C E B C E A C E B A E
200 3anrot C A E B A E C B E B A E C B E C A E
201 df-3an C A E B A E C B E C A E B A E C B E
202 prcom B A = A B
203 202 eleq1i B A E A B E
204 prcom C B = B C
205 204 eleq1i C B E B C E
206 biid C A E C A E
207 203 205 206 3anbi123i B A E C B E C A E A B E B C E C A E
208 200 201 207 3bitr3i C A E B A E C B E A B E B C E C A E
209 df-3an A B E C B E A C E A B E C B E A C E
210 biid A B E A B E
211 prcom A C = C A
212 211 eleq1i A C E C A E
213 210 205 212 3anbi123i A B E C B E A C E A B E B C E C A E
214 209 213 bitr3i A B E C B E A C E A B E B C E C A E
215 df-3an B C E A C E B A E B C E A C E B A E
216 3anrot B C E A C E B A E A C E B A E B C E
217 3anrot A C E B A E B C E B A E B C E A C E
218 biid B C E B C E
219 203 218 212 3anbi123i B A E B C E A C E A B E B C E C A E
220 216 217 219 3bitri B C E A C E B A E A B E B C E C A E
221 215 220 bitr3i B C E A C E B A E A B E B C E C A E
222 208 214 221 3anbi123i C A E B A E C B E A B E C B E A C E B C E A C E B A E A B E B C E C A E A B E B C E C A E A B E B C E C A E
223 df-3an A B E B C E C A E A B E B C E C A E A B E B C E C A E A B E B C E C A E A B E B C E C A E A B E B C E C A E
224 anabs1 A B E B C E C A E A B E B C E C A E A B E B C E C A E A B E B C E C A E A B E B C E C A E
225 anidm A B E B C E C A E A B E B C E C A E A B E B C E C A E
226 223 224 225 3bitri A B E B C E C A E A B E B C E C A E A B E B C E C A E A B E B C E C A E
227 199 222 226 3bitri C A E C B E B A E B C E A B E A C E C B E C A E B C E B A E A C E A B E A B E B C E C A E
228 180 227 bitrdi A X B Y C Z A B A C B C V = A B C G USGraph ∃! x A B C x A x B E ∃! x A B C x A x C E ∃! x A B C x B x C E ∃! x A B C x B x A E ∃! x A B C x C x A E ∃! x A B C x C x B E A B E B C E C A E
229 13 98 228 3bitrd A X B Y C Z A B A C B C V = A B C G USGraph G FriendGraph A B E B C E C A E
230 229 ex A X B Y C Z A B A C B C V = A B C G USGraph G FriendGraph A B E B C E C A E