Metamath Proof Explorer

Theorem cplgr3v

Description: A pseudograph with three (different) vertices is complete iff there is an edge between each of these three vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 5-Nov-2020) (Proof shortened by AV, 13-Feb-2022)

Ref Expression
Hypotheses cplgr3v.e ⊢E=Edg⁡G
cplgr3v.t ⊢Vtx⁡G=ABC
Assertion cplgr3v ⊢A∈X∧B∈Y∧C∈Z∧G∈UPGraph∧A≠B∧A≠C∧B≠C→G∈ComplGraph↔AB∈E∧BC∈E∧CA∈E

Proof

Step Hyp Ref Expression
1 cplgr3v.e ⊢E=Edg⁡G
2 cplgr3v.t ⊢Vtx⁡G=ABC
3 2 eqcomi ⊢ABC=Vtx⁡G
4 3 iscplgrnb ⊢G∈UPGraph→G∈ComplGraph↔∀v∈ABC∀n∈ABC∖vn∈GNeighbVtxv
5 4 3ad2ant2 ⊢A∈X∧B∈Y∧C∈Z∧G∈UPGraph∧A≠B∧A≠C∧B≠C→G∈ComplGraph↔∀v∈ABC∀n∈ABC∖vn∈GNeighbVtxv
6 sneq ⊢v=A→v=A
7 6 difeq2d ⊢v=A→ABC∖v=ABC∖A
8 tprot ⊢ABC=BCA
9 8 difeq1i ⊢ABC∖A=BCA∖A
10 necom ⊢A≠B↔B≠A
11 necom ⊢A≠C↔C≠A
12 diftpsn3 ⊢B≠A∧C≠A→BCA∖A=BC
13 10 11 12 syl2anb ⊢A≠B∧A≠C→BCA∖A=BC
14 13 3adant3 ⊢A≠B∧A≠C∧B≠C→BCA∖A=BC
15 9 14 eqtrid ⊢A≠B∧A≠C∧B≠C→ABC∖A=BC
16 15 3ad2ant3 ⊢A∈X∧B∈Y∧C∈Z∧G∈UPGraph∧A≠B∧A≠C∧B≠C→ABC∖A=BC
17 7 16 sylan9eqr ⊢A∈X∧B∈Y∧C∈Z∧G∈UPGraph∧A≠B∧A≠C∧B≠C∧v=A→ABC∖v=BC
18 oveq2 ⊢v=A→GNeighbVtxv=GNeighbVtxA
19 18 eleq2d ⊢v=A→n∈GNeighbVtxv↔n∈GNeighbVtxA
20 19 adantl ⊢A∈X∧B∈Y∧C∈Z∧G∈UPGraph∧A≠B∧A≠C∧B≠C∧v=A→n∈GNeighbVtxv↔n∈GNeighbVtxA
21 17 20 raleqbidv ⊢A∈X∧B∈Y∧C∈Z∧G∈UPGraph∧A≠B∧A≠C∧B≠C∧v=A→∀n∈ABC∖vn∈GNeighbVtxv↔∀n∈BCn∈GNeighbVtxA
22 sneq ⊢v=B→v=B
23 22 difeq2d ⊢v=B→ABC∖v=ABC∖B
24 tprot ⊢CAB=ABC
25 24 eqcomi ⊢ABC=CAB
26 25 difeq1i ⊢ABC∖B=CAB∖B
27 necom ⊢B≠C↔C≠B
28 27 biimpi ⊢B≠C→C≠B
29 28 anim2i ⊢A≠B∧B≠C→A≠B∧C≠B
30 29 ancomd ⊢A≠B∧B≠C→C≠B∧A≠B
31 diftpsn3 ⊢C≠B∧A≠B→CAB∖B=CA
32 30 31 syl ⊢A≠B∧B≠C→CAB∖B=CA
33 32 3adant2 ⊢A≠B∧A≠C∧B≠C→CAB∖B=CA
34 26 33 eqtrid ⊢A≠B∧A≠C∧B≠C→ABC∖B=CA
35 34 3ad2ant3 ⊢A∈X∧B∈Y∧C∈Z∧G∈UPGraph∧A≠B∧A≠C∧B≠C→ABC∖B=CA
36 23 35 sylan9eqr ⊢A∈X∧B∈Y∧C∈Z∧G∈UPGraph∧A≠B∧A≠C∧B≠C∧v=B→ABC∖v=CA
37 oveq2 ⊢v=B→GNeighbVtxv=GNeighbVtxB
38 37 eleq2d ⊢v=B→n∈GNeighbVtxv↔n∈GNeighbVtxB
39 38 adantl ⊢A∈X∧B∈Y∧C∈Z∧G∈UPGraph∧A≠B∧A≠C∧B≠C∧v=B→n∈GNeighbVtxv↔n∈GNeighbVtxB
40 36 39 raleqbidv ⊢A∈X∧B∈Y∧C∈Z∧G∈UPGraph∧A≠B∧A≠C∧B≠C∧v=B→∀n∈ABC∖vn∈GNeighbVtxv↔∀n∈CAn∈GNeighbVtxB
41 sneq ⊢v=C→v=C
42 41 difeq2d ⊢v=C→ABC∖v=ABC∖C
43 diftpsn3 ⊢A≠C∧B≠C→ABC∖C=AB
44 43 3adant1 ⊢A≠B∧A≠C∧B≠C→ABC∖C=AB
45 44 3ad2ant3 ⊢A∈X∧B∈Y∧C∈Z∧G∈UPGraph∧A≠B∧A≠C∧B≠C→ABC∖C=AB
46 42 45 sylan9eqr ⊢A∈X∧B∈Y∧C∈Z∧G∈UPGraph∧A≠B∧A≠C∧B≠C∧v=C→ABC∖v=AB
47 oveq2 ⊢v=C→GNeighbVtxv=GNeighbVtxC
48 47 eleq2d ⊢v=C→n∈GNeighbVtxv↔n∈GNeighbVtxC
49 48 adantl ⊢A∈X∧B∈Y∧C∈Z∧G∈UPGraph∧A≠B∧A≠C∧B≠C∧v=C→n∈GNeighbVtxv↔n∈GNeighbVtxC
50 46 49 raleqbidv ⊢A∈X∧B∈Y∧C∈Z∧G∈UPGraph∧A≠B∧A≠C∧B≠C∧v=C→∀n∈ABC∖vn∈GNeighbVtxv↔∀n∈ABn∈GNeighbVtxC
51 simp1 ⊢A∈X∧B∈Y∧C∈Z→A∈X
52 51 3ad2ant1 ⊢A∈X∧B∈Y∧C∈Z∧G∈UPGraph∧A≠B∧A≠C∧B≠C→A∈X
53 simp2 ⊢A∈X∧B∈Y∧C∈Z→B∈Y
54 53 3ad2ant1 ⊢A∈X∧B∈Y∧C∈Z∧G∈UPGraph∧A≠B∧A≠C∧B≠C→B∈Y
55 simp3 ⊢A∈X∧B∈Y∧C∈Z→C∈Z
56 55 3ad2ant1 ⊢A∈X∧B∈Y∧C∈Z∧G∈UPGraph∧A≠B∧A≠C∧B≠C→C∈Z
57 21 40 50 52 54 56 raltpd ⊢A∈X∧B∈Y∧C∈Z∧G∈UPGraph∧A≠B∧A≠C∧B≠C→∀v∈ABC∀n∈ABC∖vn∈GNeighbVtxv↔∀n∈BCn∈GNeighbVtxA∧∀n∈CAn∈GNeighbVtxB∧∀n∈ABn∈GNeighbVtxC
58 eleq1 ⊢n=B→n∈GNeighbVtxA↔B∈GNeighbVtxA
59 eleq1 ⊢n=C→n∈GNeighbVtxA↔C∈GNeighbVtxA
60 58 59 ralprg ⊢B∈Y∧C∈Z→∀n∈BCn∈GNeighbVtxA↔B∈GNeighbVtxA∧C∈GNeighbVtxA
61 60 3adant1 ⊢A∈X∧B∈Y∧C∈Z→∀n∈BCn∈GNeighbVtxA↔B∈GNeighbVtxA∧C∈GNeighbVtxA
62 eleq1 ⊢n=C→n∈GNeighbVtxB↔C∈GNeighbVtxB
63 eleq1 ⊢n=A→n∈GNeighbVtxB↔A∈GNeighbVtxB
64 62 63 ralprg ⊢C∈Z∧A∈X→∀n∈CAn∈GNeighbVtxB↔C∈GNeighbVtxB∧A∈GNeighbVtxB
65 64 ancoms ⊢A∈X∧C∈Z→∀n∈CAn∈GNeighbVtxB↔C∈GNeighbVtxB∧A∈GNeighbVtxB
66 65 3adant2 ⊢A∈X∧B∈Y∧C∈Z→∀n∈CAn∈GNeighbVtxB↔C∈GNeighbVtxB∧A∈GNeighbVtxB
67 eleq1 ⊢n=A→n∈GNeighbVtxC↔A∈GNeighbVtxC
68 eleq1 ⊢n=B→n∈GNeighbVtxC↔B∈GNeighbVtxC
69 67 68 ralprg ⊢A∈X∧B∈Y→∀n∈ABn∈GNeighbVtxC↔A∈GNeighbVtxC∧B∈GNeighbVtxC
70 69 3adant3 ⊢A∈X∧B∈Y∧C∈Z→∀n∈ABn∈GNeighbVtxC↔A∈GNeighbVtxC∧B∈GNeighbVtxC
71 61 66 70 3anbi123d ⊢A∈X∧B∈Y∧C∈Z→∀n∈BCn∈GNeighbVtxA∧∀n∈CAn∈GNeighbVtxB∧∀n∈ABn∈GNeighbVtxC↔B∈GNeighbVtxA∧C∈GNeighbVtxA∧C∈GNeighbVtxB∧A∈GNeighbVtxB∧A∈GNeighbVtxC∧B∈GNeighbVtxC
72 71 3ad2ant1 ⊢A∈X∧B∈Y∧C∈Z∧G∈UPGraph∧A≠B∧A≠C∧B≠C→∀n∈BCn∈GNeighbVtxA∧∀n∈CAn∈GNeighbVtxB∧∀n∈ABn∈GNeighbVtxC↔B∈GNeighbVtxA∧C∈GNeighbVtxA∧C∈GNeighbVtxB∧A∈GNeighbVtxB∧A∈GNeighbVtxC∧B∈GNeighbVtxC
73 3an6 ⊢B∈GNeighbVtxA∧C∈GNeighbVtxA∧C∈GNeighbVtxB∧A∈GNeighbVtxB∧A∈GNeighbVtxC∧B∈GNeighbVtxC↔B∈GNeighbVtxA∧C∈GNeighbVtxB∧A∈GNeighbVtxC∧C∈GNeighbVtxA∧A∈GNeighbVtxB∧B∈GNeighbVtxC
74 73 a1i ⊢A∈X∧B∈Y∧C∈Z∧G∈UPGraph∧A≠B∧A≠C∧B≠C→B∈GNeighbVtxA∧C∈GNeighbVtxA∧C∈GNeighbVtxB∧A∈GNeighbVtxB∧A∈GNeighbVtxC∧B∈GNeighbVtxC↔B∈GNeighbVtxA∧C∈GNeighbVtxB∧A∈GNeighbVtxC∧C∈GNeighbVtxA∧A∈GNeighbVtxB∧B∈GNeighbVtxC
75 nbgrsym ⊢B∈GNeighbVtxA↔A∈GNeighbVtxB
76 nbgrsym ⊢C∈GNeighbVtxB↔B∈GNeighbVtxC
77 nbgrsym ⊢A∈GNeighbVtxC↔C∈GNeighbVtxA
78 75 76 77 3anbi123i ⊢B∈GNeighbVtxA∧C∈GNeighbVtxB∧A∈GNeighbVtxC↔A∈GNeighbVtxB∧B∈GNeighbVtxC∧C∈GNeighbVtxA
79 78 a1i ⊢A∈X∧B∈Y∧C∈Z∧G∈UPGraph∧A≠B∧A≠C∧B≠C→B∈GNeighbVtxA∧C∈GNeighbVtxB∧A∈GNeighbVtxC↔A∈GNeighbVtxB∧B∈GNeighbVtxC∧C∈GNeighbVtxA
80 79 anbi1d ⊢A∈X∧B∈Y∧C∈Z∧G∈UPGraph∧A≠B∧A≠C∧B≠C→B∈GNeighbVtxA∧C∈GNeighbVtxB∧A∈GNeighbVtxC∧C∈GNeighbVtxA∧A∈GNeighbVtxB∧B∈GNeighbVtxC↔A∈GNeighbVtxB∧B∈GNeighbVtxC∧C∈GNeighbVtxA∧C∈GNeighbVtxA∧A∈GNeighbVtxB∧B∈GNeighbVtxC
81 3anrot ⊢C∈GNeighbVtxA∧A∈GNeighbVtxB∧B∈GNeighbVtxC↔A∈GNeighbVtxB∧B∈GNeighbVtxC∧C∈GNeighbVtxA
82 81 bicomi ⊢A∈GNeighbVtxB∧B∈GNeighbVtxC∧C∈GNeighbVtxA↔C∈GNeighbVtxA∧A∈GNeighbVtxB∧B∈GNeighbVtxC
83 82 anbi1i ⊢A∈GNeighbVtxB∧B∈GNeighbVtxC∧C∈GNeighbVtxA∧C∈GNeighbVtxA∧A∈GNeighbVtxB∧B∈GNeighbVtxC↔C∈GNeighbVtxA∧A∈GNeighbVtxB∧B∈GNeighbVtxC∧C∈GNeighbVtxA∧A∈GNeighbVtxB∧B∈GNeighbVtxC
84 anidm ⊢C∈GNeighbVtxA∧A∈GNeighbVtxB∧B∈GNeighbVtxC∧C∈GNeighbVtxA∧A∈GNeighbVtxB∧B∈GNeighbVtxC↔C∈GNeighbVtxA∧A∈GNeighbVtxB∧B∈GNeighbVtxC
85 83 84 bitri ⊢A∈GNeighbVtxB∧B∈GNeighbVtxC∧C∈GNeighbVtxA∧C∈GNeighbVtxA∧A∈GNeighbVtxB∧B∈GNeighbVtxC↔C∈GNeighbVtxA∧A∈GNeighbVtxB∧B∈GNeighbVtxC
86 85 a1i ⊢A∈X∧B∈Y∧C∈Z∧G∈UPGraph∧A≠B∧A≠C∧B≠C→A∈GNeighbVtxB∧B∈GNeighbVtxC∧C∈GNeighbVtxA∧C∈GNeighbVtxA∧A∈GNeighbVtxB∧B∈GNeighbVtxC↔C∈GNeighbVtxA∧A∈GNeighbVtxB∧B∈GNeighbVtxC
87 tpid1g ⊢A∈X→A∈ABC
88 tpid2g ⊢B∈Y→B∈ABC
89 tpid3g ⊢C∈Z→C∈ABC
90 87 88 89 3anim123i ⊢A∈X∧B∈Y∧C∈Z→A∈ABC∧B∈ABC∧C∈ABC
91 df-3an ⊢A∈ABC∧B∈ABC∧C∈ABC↔A∈ABC∧B∈ABC∧C∈ABC
92 90 91 sylib ⊢A∈X∧B∈Y∧C∈Z→A∈ABC∧B∈ABC∧C∈ABC
93 simplr ⊢A∈ABC∧B∈ABC∧C∈ABC→B∈ABC
94 93 anim1ci ⊢A∈ABC∧B∈ABC∧C∈ABC∧G∈UPGraph→G∈UPGraph∧B∈ABC
95 94 3adant3 ⊢A∈ABC∧B∈ABC∧C∈ABC∧G∈UPGraph∧A≠B∧A≠C∧B≠C→G∈UPGraph∧B∈ABC
96 simpll ⊢A∈ABC∧B∈ABC∧C∈ABC→A∈ABC
97 simp1 ⊢A≠B∧A≠C∧B≠C→A≠B
98 96 97 anim12i ⊢A∈ABC∧B∈ABC∧C∈ABC∧A≠B∧A≠C∧B≠C→A∈ABC∧A≠B
99 3 1 nbupgrel ⊢G∈UPGraph∧B∈ABC∧A∈ABC∧A≠B→A∈GNeighbVtxB↔AB∈E
100 95 98 99 3imp3i2an ⊢A∈ABC∧B∈ABC∧C∈ABC∧G∈UPGraph∧A≠B∧A≠C∧B≠C→A∈GNeighbVtxB↔AB∈E
101 simpr ⊢A∈ABC∧B∈ABC∧C∈ABC→C∈ABC
102 101 anim1ci ⊢A∈ABC∧B∈ABC∧C∈ABC∧G∈UPGraph→G∈UPGraph∧C∈ABC
103 102 3adant3 ⊢A∈ABC∧B∈ABC∧C∈ABC∧G∈UPGraph∧A≠B∧A≠C∧B≠C→G∈UPGraph∧C∈ABC
104 simp3 ⊢A≠B∧A≠C∧B≠C→B≠C
105 93 104 anim12i ⊢A∈ABC∧B∈ABC∧C∈ABC∧A≠B∧A≠C∧B≠C→B∈ABC∧B≠C
106 3 1 nbupgrel ⊢G∈UPGraph∧C∈ABC∧B∈ABC∧B≠C→B∈GNeighbVtxC↔BC∈E
107 103 105 106 3imp3i2an ⊢A∈ABC∧B∈ABC∧C∈ABC∧G∈UPGraph∧A≠B∧A≠C∧B≠C→B∈GNeighbVtxC↔BC∈E
108 96 anim1ci ⊢A∈ABC∧B∈ABC∧C∈ABC∧G∈UPGraph→G∈UPGraph∧A∈ABC
109 108 3adant3 ⊢A∈ABC∧B∈ABC∧C∈ABC∧G∈UPGraph∧A≠B∧A≠C∧B≠C→G∈UPGraph∧A∈ABC
110 simp2 ⊢A≠B∧A≠C∧B≠C→A≠C
111 110 necomd ⊢A≠B∧A≠C∧B≠C→C≠A
112 101 111 anim12i ⊢A∈ABC∧B∈ABC∧C∈ABC∧A≠B∧A≠C∧B≠C→C∈ABC∧C≠A
113 3 1 nbupgrel ⊢G∈UPGraph∧A∈ABC∧C∈ABC∧C≠A→C∈GNeighbVtxA↔CA∈E
114 109 112 113 3imp3i2an ⊢A∈ABC∧B∈ABC∧C∈ABC∧G∈UPGraph∧A≠B∧A≠C∧B≠C→C∈GNeighbVtxA↔CA∈E
115 100 107 114 3anbi123d ⊢A∈ABC∧B∈ABC∧C∈ABC∧G∈UPGraph∧A≠B∧A≠C∧B≠C→A∈GNeighbVtxB∧B∈GNeighbVtxC∧C∈GNeighbVtxA↔AB∈E∧BC∈E∧CA∈E
116 92 115 syl3an1 ⊢A∈X∧B∈Y∧C∈Z∧G∈UPGraph∧A≠B∧A≠C∧B≠C→A∈GNeighbVtxB∧B∈GNeighbVtxC∧C∈GNeighbVtxA↔AB∈E∧BC∈E∧CA∈E
117 81 116 bitrid ⊢A∈X∧B∈Y∧C∈Z∧G∈UPGraph∧A≠B∧A≠C∧B≠C→C∈GNeighbVtxA∧A∈GNeighbVtxB∧B∈GNeighbVtxC↔AB∈E∧BC∈E∧CA∈E
118 80 86 117 3bitrd ⊢A∈X∧B∈Y∧C∈Z∧G∈UPGraph∧A≠B∧A≠C∧B≠C→B∈GNeighbVtxA∧C∈GNeighbVtxB∧A∈GNeighbVtxC∧C∈GNeighbVtxA∧A∈GNeighbVtxB∧B∈GNeighbVtxC↔AB∈E∧BC∈E∧CA∈E
119 72 74 118 3bitrd ⊢A∈X∧B∈Y∧C∈Z∧G∈UPGraph∧A≠B∧A≠C∧B≠C→∀n∈BCn∈GNeighbVtxA∧∀n∈CAn∈GNeighbVtxB∧∀n∈ABn∈GNeighbVtxC↔AB∈E∧BC∈E∧CA∈E
120 5 57 119 3bitrd ⊢A∈X∧B∈Y∧C∈Z∧G∈UPGraph∧A≠B∧A≠C∧B≠C→G∈ComplGraph↔AB∈E∧BC∈E∧CA∈E