Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cusgra3v Structured version   Visualization version   Unicode version

Theorem cusgra3v 25271
 Description: A graph with three (different) vertices is complete if and only if there is an edge between each of these three vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
Hypothesis
Ref Expression
cusgra3v.v
Assertion
Ref Expression
cusgra3v USGrph ComplUSGrph

Proof of Theorem cusgra3v
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp2 1031 . . 3 USGrph USGrph
21biantrurd 516 . 2 USGrph USGrph
3 cusgra3v.v . . . . . . . 8
43difeq1i 3536 . . . . . . 7
54a1i 11 . . . . . 6 USGrph
65raleqdv 2979 . . . . 5 USGrph
76ralbidv 2829 . . . 4 USGrph
83raleqi 2977 . . . . 5
98a1i 11 . . . 4 USGrph
10 sneq 3969 . . . . . . . 8
1110difeq2d 3540 . . . . . . 7
12 preq2 4043 . . . . . . . 8
1312eleq1d 2533 . . . . . . 7
1411, 13raleqbidv 2987 . . . . . 6
15 sneq 3969 . . . . . . . 8
1615difeq2d 3540 . . . . . . 7
17 preq2 4043 . . . . . . . 8
1817eleq1d 2533 . . . . . . 7
1916, 18raleqbidv 2987 . . . . . 6
20 sneq 3969 . . . . . . . 8
2120difeq2d 3540 . . . . . . 7
22 preq2 4043 . . . . . . . 8
2322eleq1d 2533 . . . . . . 7
2421, 23raleqbidv 2987 . . . . . 6
2514, 19, 24raltpg 4014 . . . . 5
26253ad2ant1 1051 . . . 4 USGrph
277, 9, 263bitrd 287 . . 3 USGrph
28 tprot 4058 . . . . . . . . 9
2928a1i 11 . . . . . . . 8
3029difeq1d 3539 . . . . . . 7
31 necom 2696 . . . . . . . . . . 11
32 necom 2696 . . . . . . . . . . 11
3331, 32anbi12i 711 . . . . . . . . . 10
3433biimpi 199 . . . . . . . . 9
35343adant3 1050 . . . . . . . 8
36 diftpsn3 4101 . . . . . . . 8
3735, 36syl 17 . . . . . . 7
3830, 37eqtrd 2505 . . . . . 6
39383ad2ant3 1053 . . . . 5 USGrph
4039raleqdv 2979 . . . 4 USGrph
41 tpcomb 4060 . . . . . . . . 9
4241a1i 11 . . . . . . . 8
4342difeq1d 3539 . . . . . . 7
44 necom 2696 . . . . . . . . . . 11
4544biimpi 199 . . . . . . . . . 10
4645anim2i 579 . . . . . . . . 9
47463adant2 1049 . . . . . . . 8
48 diftpsn3 4101 . . . . . . . 8
4947, 48syl 17 . . . . . . 7
5043, 49eqtrd 2505 . . . . . 6
51503ad2ant3 1053 . . . . 5 USGrph
5251raleqdv 2979 . . . 4 USGrph
53 diftpsn3 4101 . . . . . . 7
54533adant1 1048 . . . . . 6
55543ad2ant3 1053 . . . . 5 USGrph
5655raleqdv 2979 . . . 4 USGrph
5740, 52, 563anbi123d 1365 . . 3 USGrph
58 preq1 4042 . . . . . . . . 9
5958eleq1d 2533 . . . . . . . 8
60 preq1 4042 . . . . . . . . 9
6160eleq1d 2533 . . . . . . . 8
6259, 61ralprg 4012 . . . . . . 7
63623adant1 1048 . . . . . 6
64633ad2ant1 1051 . . . . 5 USGrph
65 preq1 4042 . . . . . . . . 9
6665eleq1d 2533 . . . . . . . 8
67 preq1 4042 . . . . . . . . 9
6867eleq1d 2533 . . . . . . . 8
6966, 68ralprg 4012 . . . . . . 7
70693adant2 1049 . . . . . 6
71703ad2ant1 1051 . . . . 5 USGrph
72 preq1 4042 . . . . . . . . 9
7372eleq1d 2533 . . . . . . . 8
74 preq1 4042 . . . . . . . . 9
7574eleq1d 2533 . . . . . . . 8
7673, 75ralprg 4012 . . . . . . 7
77763adant3 1050 . . . . . 6
78773ad2ant1 1051 . . . . 5 USGrph
7964, 71, 783anbi123d 1365 . . . 4 USGrph
80 ancom 457 . . . . . . 7
81803anbi2i 1222 . . . . . 6
82 3an6 1375 . . . . . 6
8381, 82bitri 257 . . . . 5
8483a1i 11 . . . 4 USGrph
85 prcom 4041 . . . . . . . . 9
8685eleq1i 2540 . . . . . . . 8
87 prcom 4041 . . . . . . . . 9
8887eleq1i 2540 . . . . . . . 8
89 prcom 4041 . . . . . . . . 9
9089eleq1i 2540 . . . . . . . 8
9186, 88, 903anbi123i 1219 . . . . . . 7
92 3anrot 1012 . . . . . . 7
9391, 92anbi12i 711 . . . . . 6
94 anidm 656 . . . . . 6
9593, 94bitri 257 . . . . 5
9695a1i 11 . . . 4 USGrph
9779, 84, 963bitrd 287 . . 3 USGrph
9827, 57, 973bitrrd 288 . 2 USGrph
99 usgrav 25144 . . . 4 USGrph
100 iscusgra 25263 . . . 4 ComplUSGrph USGrph
10199, 100syl 17 . . 3 USGrph ComplUSGrph USGrph
1021013ad2ant2 1052 . 2 USGrph ComplUSGrph USGrph
1032, 98, 1023bitr4rd 294 1 USGrph ComplUSGrph
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 189   wa 376   w3a 1007   wceq 1452   wcel 1904   wne 2641  wral 2756  cvv 3031   cdif 3387  csn 3959  cpr 3961  ctp 3963   class class class wbr 4395   crn 4840   USGrph cusg 25136   ComplUSGrph ccusgra 25225 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pr 4639 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-sbc 3256  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-br 4396  df-opab 4455  df-xp 4845  df-rel 4846  df-cnv 4847  df-dm 4849  df-rn 4850  df-usgra 25139  df-cusgra 25228 This theorem is referenced by:  cusgra3vnbpr  25272
 Copyright terms: Public domain W3C validator