# 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}=\mathrm{Edg}\left({G}\right)$
cplgr3v.t ${⊢}\mathrm{Vtx}\left({G}\right)=\left\{{A},{B},{C}\right\}$
Assertion cplgr3v ${⊢}\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {C}\in {Z}\right)\wedge {G}\in \mathrm{UPGraph}\wedge \left({A}\ne {B}\wedge {A}\ne {C}\wedge {B}\ne {C}\right)\right)\to \left({G}\in \mathrm{ComplGraph}↔\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\wedge \left\{{C},{A}\right\}\in {E}\right)\right)$

### Proof

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