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 = A B C
Assertion cplgr3v ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ G ∈ UPGraph ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → G ∈ ComplGraph ↔ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E

Proof

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