Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  frgra3v Unicode version

Theorem frgra3v 28191
 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.)
Assertion
Ref Expression
frgra3v USGrph FriendGrph

Proof of Theorem frgra3v
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 usgrav 28112 . . . . . 6 USGrph
2 isfrgra 28182 . . . . . 6 FriendGrph USGrph
31, 2syl 15 . . . . 5 USGrph FriendGrph USGrph
43adantl 452 . . . 4 USGrph FriendGrph USGrph
5 ibar 490 . . . . 5 USGrph USGrph
65adantl 452 . . . 4 USGrph USGrph
74, 6bitr4d 247 . . 3 USGrph FriendGrph
8 sneq 3653 . . . . . . . . 9
98difeq2d 3296 . . . . . . . 8
10 preq2 3709 . . . . . . . . . . 11
1110preq1d 3714 . . . . . . . . . 10
1211sseq1d 3207 . . . . . . . . 9
1312reubidv 2726 . . . . . . . 8
149, 13raleqbidv 2750 . . . . . . 7
15 sneq 3653 . . . . . . . . 9
1615difeq2d 3296 . . . . . . . 8
17 preq2 3709 . . . . . . . . . . 11
1817preq1d 3714 . . . . . . . . . 10
1918sseq1d 3207 . . . . . . . . 9
2019reubidv 2726 . . . . . . . 8
2116, 20raleqbidv 2750 . . . . . . 7
22 sneq 3653 . . . . . . . . 9
2322difeq2d 3296 . . . . . . . 8
24 preq2 3709 . . . . . . . . . . 11
2524preq1d 3714 . . . . . . . . . 10
2625sseq1d 3207 . . . . . . . . 9
2726reubidv 2726 . . . . . . . 8
2823, 27raleqbidv 2750 . . . . . . 7
2914, 21, 28raltpg 3686 . . . . . 6
3029adantr 451 . . . . 5
3130adantr 451 . . . 4 USGrph
32 tprot 3724 . . . . . . . . . . 11
3332a1i 10 . . . . . . . . . 10
3433difeq1d 3295 . . . . . . . . 9
35 necom 2529 . . . . . . . . . . . . 13
3635biimpi 186 . . . . . . . . . . . 12
37 necom 2529 . . . . . . . . . . . . 13
3837biimpi 186 . . . . . . . . . . . 12
3936, 38anim12i 549 . . . . . . . . . . 11
40393adant3 975 . . . . . . . . . 10
41 diftpsneq 28081 . . . . . . . . . 10
4240, 41syl 15 . . . . . . . . 9
4334, 42eqtrd 2317 . . . . . . . 8
4443raleqdv 2744 . . . . . . 7
45 tprot 3724 . . . . . . . . . . . 12
4645eqcomi 2289 . . . . . . . . . . 11
4746a1i 10 . . . . . . . . . 10
4847difeq1d 3295 . . . . . . . . 9
49 id 19 . . . . . . . . . . . 12
50 necom 2529 . . . . . . . . . . . . 13
5150biimpi 186 . . . . . . . . . . . 12
5249, 51anim12ci 550 . . . . . . . . . . 11
53523adant2 974 . . . . . . . . . 10
54 diftpsneq 28081 . . . . . . . . . 10
5553, 54syl 15 . . . . . . . . 9
5648, 55eqtrd 2317 . . . . . . . 8
5756raleqdv 2744 . . . . . . 7
58 diftpsneq 28081 . . . . . . . . 9
59583adant1 973 . . . . . . . 8
6059raleqdv 2744 . . . . . . 7
6144, 57, 603anbi123d 1252 . . . . . 6
6261adantl 452 . . . . 5
6362adantr 451 . . . 4 USGrph
64 preq2 3709 . . . . . . . . . . . 12
6564preq2d 3715 . . . . . . . . . . 11
6665sseq1d 3207 . . . . . . . . . 10
6766reubidv 2726 . . . . . . . . 9
68 preq2 3709 . . . . . . . . . . . 12
6968preq2d 3715 . . . . . . . . . . 11
7069sseq1d 3207 . . . . . . . . . 10
7170reubidv 2726 . . . . . . . . 9
7267, 71ralprg 3684 . . . . . . . 8
73723adant1 973 . . . . . . 7
7468preq2d 3715 . . . . . . . . . . . 12
7574sseq1d 3207 . . . . . . . . . . 11
7675reubidv 2726 . . . . . . . . . 10
77 preq2 3709 . . . . . . . . . . . . 13
7877preq2d 3715 . . . . . . . . . . . 12
7978sseq1d 3207 . . . . . . . . . . 11
8079reubidv 2726 . . . . . . . . . 10
8176, 80ralprg 3684 . . . . . . . . 9
8281ancoms 439 . . . . . . . 8
83823adant2 974 . . . . . . 7
8477preq2d 3715 . . . . . . . . . . 11
8584sseq1d 3207 . . . . . . . . . 10
8685reubidv 2726 . . . . . . . . 9
8764preq2d 3715 . . . . . . . . . . 11
8887sseq1d 3207 . . . . . . . . . 10
8988reubidv 2726 . . . . . . . . 9
9086, 89ralprg 3684 . . . . . . . 8
91903adant3 975 . . . . . . 7
9273, 83, 913anbi123d 1252 . . . . . 6
9392adantr 451 . . . . 5
9493adantr 451 . . . 4 USGrph
9531, 63, 943bitrd 270 . . 3 USGrph
96 frgra3vlem2 28190 . . . . . . 7 USGrph
9796imp 418 . . . . . 6 USGrph
98 3ancomb 943 . . . . . . . 8
99 3ancoma 941 . . . . . . . . 9
100 biid 227 . . . . . . . . . 10
101 biid 227 . . . . . . . . . 10
102100, 101, 503anbi123i 1140 . . . . . . . . 9
10399, 102bitri 240 . . . . . . . 8
10498, 103anbi12i 678 . . . . . . 7
105 tpcomb 3726 . . . . . . . 8
106105breq1i 4032 . . . . . . 7 USGrph USGrph
107 reueq1 2740 . . . . . . . . 9
108105, 107mp1i 11 . . . . . . . 8 USGrph
109 frgra3vlem2 28190 . . . . . . . . 9 USGrph
110109imp 418 . . . . . . . 8 USGrph
111108, 110bitrd 244 . . . . . . 7 USGrph
112104, 106, 111syl2anb 465 . . . . . 6 USGrph
11397, 112anbi12d 691 . . . . 5 USGrph
114 3anrot 939 . . . . . . . 8
115 3anrot 939 . . . . . . . . 9
116 biid 227 . . . . . . . . . 10
117116, 35, 373anbi123i 1140 . . . . . . . . 9
118115, 117bitr3i 242 . . . . . . . 8
119114, 118anbi12i 678 . . . . . . 7
12032breq1i 4032 . . . . . . 7 USGrph USGrph
121 reueq1 2740 . . . . . . . . 9
12232, 121mp1i 11 . . . . . . . 8 USGrph
123 frgra3vlem2 28190 . . . . . . . . 9 USGrph
124123imp 418 . . . . . . . 8 USGrph
125122, 124bitrd 244 . . . . . . 7 USGrph
126119, 120, 125syl2anb 465 . . . . . 6 USGrph
127 3ancoma 941 . . . . . . . 8
128 3ancomb 943 . . . . . . . . 9
12935, 116, 1003anbi123i 1140 . . . . . . . . 9
130128, 129bitri 240 . . . . . . . 8
131127, 130anbi12i 678 . . . . . . 7
132 tpcoma 3725 . . . . . . . 8
133132breq1i 4032 . . . . . . 7 USGrph USGrph
134 reueq1 2740 . . . . . . . . 9
135132, 134mp1i 11 . . . . . . . 8 USGrph
136 frgra3vlem2 28190 . . . . . . . . 9 USGrph
137136imp 418 . . . . . . . 8 USGrph
138135, 137bitrd 244 . . . . . . 7 USGrph
139131, 133, 138syl2anb 465 . . . . . 6 USGrph
140126, 139anbi12d 691 . . . . 5 USGrph
141 3anrot 939 . . . . . . . . . 10
142141bicomi 193 . . . . . . . . 9
143142biimpi 186 . . . . . . . 8
144 3anrot 939 . . . . . . . . . 10
14537, 50, 1013anbi123i 1140 . . . . . . . . . 10
146144, 145bitri 240 . . . . . . . . 9
147146biimpi 186 . . . . . . . 8
148143, 147anim12i 549 . . . . . . 7
14946breq1i 4032 . . . . . . . 8 USGrph USGrph
150149biimpi 186 . . . . . . 7 USGrph USGrph
151 reueq1 2740 . . . . . . . . 9
15246, 151mp1i 11 . . . . . . . 8 USGrph
153 frgra3vlem2 28190 . . . . . . . . 9 USGrph
154153imp 418 . . . . . . . 8 USGrph
155152, 154bitrd 244 . . . . . . 7 USGrph
156148, 150, 155syl2an 463 . . . . . 6 USGrph
157 3anrev 945 . . . . . . . . 9
158157biimpi 186 . . . . . . . 8
15950, 37, 353anbi123i 1140 . . . . . . . . . 10
160159biimpi 186 . . . . . . . . 9
1611603com13 1156 . . . . . . . 8
162158, 161anim12i 549 . . . . . . 7
163 tpcoma 3725 . . . . . . . . . 10
16432, 163eqtri 2305 . . . . . . . . 9
165164breq1i 4032 . . . . . . . 8 USGrph USGrph
166165biimpi 186 . . . . . . 7 USGrph USGrph
167 reueq1 2740 . . . . . . . . 9
168164, 167mp1i 11 . . . . . . . 8 USGrph
169 frgra3vlem2 28190 . . . . . . . . 9 USGrph
170169imp 418 . . . . . . . 8 USGrph
171168, 170bitrd 244 . . . . . . 7 USGrph
172162, 166, 171syl2an 463 . . . . . 6 USGrph
173156, 172anbi12d 691 . . . . 5 USGrph
174113, 140, 1733anbi123d 1252 . . . 4 USGrph
175 prcom 3707 . . . . . . . . . . 11
176175eleq1i 2348 . . . . . . . . . 10
177176anbi2i 675 . . . . . . . . 9
178177anbi2i 675 . . . . . . . 8
179 anandir 802 . . . . . . . 8
180178, 179bitr4i 243 . . . . . . 7
181 prcom 3707 . . . . . . . . . . 11
182181eleq1i 2348 . . . . . . . . . 10
183182anbi2i 675 . . . . . . . . 9
184183anbi2i 675 . . . . . . . 8
185 anandir 802 . . . . . . . 8
186184, 185bitr4i 243 . . . . . . 7
187 prcom 3707 . . . . . . . . . . 11
188187eleq1i 2348 . . . . . . . . . 10
189188anbi2i 675 . . . . . . . . 9
190189anbi2i 675 . . . . . . . 8
191 anandir 802 . . . . . . . 8
192190, 191bitr4i 243 . . . . . . 7
193180, 186, 1923anbi123i 1140 . . . . . 6
194 df-3an 936 . . . . . . . 8
195 3anrot 939 . . . . . . . . 9
196 prcom 3707 . . . . . . . . . . 11
197196eleq1i 2348 . . . . . . . . . 10
198 prcom 3707 . . . . . . . . . . 11
199198eleq1i 2348 . . . . . . . . . 10
200 biid 227 . . . . . . . . . 10
201197, 199, 2003anbi123i 1140 . . . . . . . . 9
202195, 201bitri 240 . . . . . . . 8
203194, 202bitr3i 242 . . . . . . 7
204 df-3an 936 . . . . . . . 8
205 biid 227 . . . . . . . . 9
206 prcom 3707 . . . . . . . . . 10
207206eleq1i 2348 . . . . . . . . 9
208205, 199, 2073anbi123i 1140 . . . . . . . 8
209204, 208bitr3i 242 . . . . . . 7
210 df-3an 936 . . . . . . . 8
211 3anrot 939 . . . . . . . . 9
212 3anrot 939 . . . . . . . . 9
213 biid 227 . . . . . . . . . 10
214197, 213, 2073anbi123i 1140 . . . . . . . . 9
215211, 212, 2143bitri 262 . . . . . . . 8
216210, 215bitr3i 242 . . . . . . 7
217203, 209, 2163anbi123i 1140 . . . . . 6
218 df-3an 936 . . . . . . 7
219 anabs1 783 . . . . . . 7
220 anidm 625 . . . . . . 7
221218, 219, 2203bitri 262 . . . . . 6
222193, 217, 2213bitri 262 . . . . 5
223222a1i 10 . . . 4 USGrph
224174, 223bitrd 244 . . 3 USGrph
2257, 95, 2243bitrd 270 . 2 USGrph FriendGrph
226225ex 423 1 USGrph FriendGrph
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   w3a 934   wceq 1625   wcel 1686   wne 2448  wral 2545  wreu 2547  cvv 2790   cdif 3151   wss 3154  csn 3642  cpr 3643  ctp 3644   class class class wbr 4025   crn 4692   USGrph cusg 28106   FriendGrph cfrgra 28180 This theorem is referenced by:  3vfriswmgra  28194 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-rep 4133  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216  ax-un 4514  ax-cnex 8795  ax-resscn 8796  ax-1cn 8797  ax-icn 8798  ax-addcl 8799  ax-addrcl 8800  ax-mulcl 8801  ax-mulrcl 8802  ax-mulcom 8803  ax-addass 8804  ax-mulass 8805  ax-distr 8806  ax-i2m1 8807  ax-1ne0 8808  ax-1rid 8809  ax-rnegex 8810  ax-rrecex 8811  ax-cnre 8812  ax-pre-lttri 8813  ax-pre-lttrn 8814  ax-pre-ltadd 8815  ax-pre-mulgt0 8816 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-nel 2451  df-ral 2550  df-rex 2551  df-reu 2552  df-rmo 2553  df-rab 2554  df-v 2792  df-sbc 2994  df-csb 3084  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-pss 3170  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-tp 3650  df-op 3651  df-uni 3830  df-int 3865  df-iun 3909  df-br 4026  df-opab 4080  df-mpt 4081  df-tr 4116  df-eprel 4307  df-id 4311  df-po 4316  df-so 4317  df-fr 4354  df-we 4356  df-ord 4397  df-on 4398  df-lim 4399  df-suc 4400  df-om 4659  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-res 4703  df-ima 4704  df-iota 5221  df-fun 5259  df-fn 5260  df-f 5261  df-f1 5262  df-fo 5263  df-f1o 5264  df-fv 5265  df-ov 5863  df-oprab 5864  df-mpt2 5865  df-1st 6124  df-2nd 6125  df-riota 6306  df-recs 6390  df-rdg 6425  df-1o 6481  df-oadd 6485  df-er 6662  df-en 6866  df-dom 6867  df-sdom 6868  df-fin 6869  df-card 7574  df-cda 7796  df-pnf 8871  df-mnf 8872  df-xr 8873  df-ltxr 8874  df-le 8875  df-sub 9041  df-neg 9042  df-nn 9749  df-2 9806  df-n0 9968  df-z 10027  df-uz 10233  df-fz 10785  df-hash 11340  df-usgra 28108  df-frgra 28181
 Copyright terms: Public domain W3C validator