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 e. X /\ B e. Y /\ C e. Z ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( G e. ComplGraph <-> ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. 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 e. UPGraph -> ( G e. ComplGraph <-> A. v e. { A , B , C } A. n e. ( { A , B , C } \ { v } ) n e. ( G NeighbVtx v ) ) )
5 4 3ad2ant2 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( G e. ComplGraph <-> A. v e. { A , B , C } A. n e. ( { A , B , C } \ { v } ) n e. ( 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 eqtrid 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { A } ) = { B , C } )
16 15 3ad2ant3 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( { A , B , C } \ { A } ) = { B , C } )
17 7 16 sylan9eqr 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. 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 e. ( G NeighbVtx v ) <-> n e. ( G NeighbVtx A ) ) )
20 19 adantl 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ v = A ) -> ( n e. ( G NeighbVtx v ) <-> n e. ( G NeighbVtx A ) ) )
21 17 20 raleqbidv 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ v = A ) -> ( A. n e. ( { A , B , C } \ { v } ) n e. ( G NeighbVtx v ) <-> A. n e. { B , C } n e. ( 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 eqtrid 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { B } ) = { C , A } )
35 34 3ad2ant3 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( { A , B , C } \ { B } ) = { C , A } )
36 23 35 sylan9eqr 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. 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 e. ( G NeighbVtx v ) <-> n e. ( G NeighbVtx B ) ) )
39 38 adantl 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ v = B ) -> ( n e. ( G NeighbVtx v ) <-> n e. ( G NeighbVtx B ) ) )
40 36 39 raleqbidv 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ v = B ) -> ( A. n e. ( { A , B , C } \ { v } ) n e. ( G NeighbVtx v ) <-> A. n e. { C , A } n e. ( 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 e. X /\ B e. Y /\ C e. Z ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( { A , B , C } \ { C } ) = { A , B } )
46 42 45 sylan9eqr 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. 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 e. ( G NeighbVtx v ) <-> n e. ( G NeighbVtx C ) ) )
49 48 adantl 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ v = C ) -> ( n e. ( G NeighbVtx v ) <-> n e. ( G NeighbVtx C ) ) )
50 46 49 raleqbidv 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ v = C ) -> ( A. n e. ( { A , B , C } \ { v } ) n e. ( G NeighbVtx v ) <-> A. n e. { A , B } n e. ( G NeighbVtx C ) ) )
51 simp1 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> A e. X )
52 51 3ad2ant1 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> A e. X )
53 simp2 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> B e. Y )
54 53 3ad2ant1 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> B e. Y )
55 simp3 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> C e. Z )
56 55 3ad2ant1 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> C e. Z )
57 21 40 50 52 54 56 raltpd 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( A. v e. { A , B , C } A. n e. ( { A , B , C } \ { v } ) n e. ( G NeighbVtx v ) <-> ( A. n e. { B , C } n e. ( G NeighbVtx A ) /\ A. n e. { C , A } n e. ( G NeighbVtx B ) /\ A. n e. { A , B } n e. ( G NeighbVtx C ) ) ) )
58 eleq1 
 |-  ( n = B -> ( n e. ( G NeighbVtx A ) <-> B e. ( G NeighbVtx A ) ) )
59 eleq1 
 |-  ( n = C -> ( n e. ( G NeighbVtx A ) <-> C e. ( G NeighbVtx A ) ) )
60 58 59 ralprg 
 |-  ( ( B e. Y /\ C e. Z ) -> ( A. n e. { B , C } n e. ( G NeighbVtx A ) <-> ( B e. ( G NeighbVtx A ) /\ C e. ( G NeighbVtx A ) ) ) )
61 60 3adant1 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( A. n e. { B , C } n e. ( G NeighbVtx A ) <-> ( B e. ( G NeighbVtx A ) /\ C e. ( G NeighbVtx A ) ) ) )
62 eleq1 
 |-  ( n = C -> ( n e. ( G NeighbVtx B ) <-> C e. ( G NeighbVtx B ) ) )
63 eleq1 
 |-  ( n = A -> ( n e. ( G NeighbVtx B ) <-> A e. ( G NeighbVtx B ) ) )
64 62 63 ralprg 
 |-  ( ( C e. Z /\ A e. X ) -> ( A. n e. { C , A } n e. ( G NeighbVtx B ) <-> ( C e. ( G NeighbVtx B ) /\ A e. ( G NeighbVtx B ) ) ) )
65 64 ancoms 
 |-  ( ( A e. X /\ C e. Z ) -> ( A. n e. { C , A } n e. ( G NeighbVtx B ) <-> ( C e. ( G NeighbVtx B ) /\ A e. ( G NeighbVtx B ) ) ) )
66 65 3adant2 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( A. n e. { C , A } n e. ( G NeighbVtx B ) <-> ( C e. ( G NeighbVtx B ) /\ A e. ( G NeighbVtx B ) ) ) )
67 eleq1 
 |-  ( n = A -> ( n e. ( G NeighbVtx C ) <-> A e. ( G NeighbVtx C ) ) )
68 eleq1 
 |-  ( n = B -> ( n e. ( G NeighbVtx C ) <-> B e. ( G NeighbVtx C ) ) )
69 67 68 ralprg 
 |-  ( ( A e. X /\ B e. Y ) -> ( A. n e. { A , B } n e. ( G NeighbVtx C ) <-> ( A e. ( G NeighbVtx C ) /\ B e. ( G NeighbVtx C ) ) ) )
70 69 3adant3 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( A. n e. { A , B } n e. ( G NeighbVtx C ) <-> ( A e. ( G NeighbVtx C ) /\ B e. ( G NeighbVtx C ) ) ) )
71 61 66 70 3anbi123d 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( ( A. n e. { B , C } n e. ( G NeighbVtx A ) /\ A. n e. { C , A } n e. ( G NeighbVtx B ) /\ A. n e. { A , B } n e. ( G NeighbVtx C ) ) <-> ( ( B e. ( G NeighbVtx A ) /\ C e. ( G NeighbVtx A ) ) /\ ( C e. ( G NeighbVtx B ) /\ A e. ( G NeighbVtx B ) ) /\ ( A e. ( G NeighbVtx C ) /\ B e. ( G NeighbVtx C ) ) ) ) )
72 71 3ad2ant1 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( A. n e. { B , C } n e. ( G NeighbVtx A ) /\ A. n e. { C , A } n e. ( G NeighbVtx B ) /\ A. n e. { A , B } n e. ( G NeighbVtx C ) ) <-> ( ( B e. ( G NeighbVtx A ) /\ C e. ( G NeighbVtx A ) ) /\ ( C e. ( G NeighbVtx B ) /\ A e. ( G NeighbVtx B ) ) /\ ( A e. ( G NeighbVtx C ) /\ B e. ( G NeighbVtx C ) ) ) ) )
73 3an6 
 |-  ( ( ( B e. ( G NeighbVtx A ) /\ C e. ( G NeighbVtx A ) ) /\ ( C e. ( G NeighbVtx B ) /\ A e. ( G NeighbVtx B ) ) /\ ( A e. ( G NeighbVtx C ) /\ B e. ( G NeighbVtx C ) ) ) <-> ( ( B e. ( G NeighbVtx A ) /\ C e. ( G NeighbVtx B ) /\ A e. ( G NeighbVtx C ) ) /\ ( C e. ( G NeighbVtx A ) /\ A e. ( G NeighbVtx B ) /\ B e. ( G NeighbVtx C ) ) ) )
74 73 a1i 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( ( B e. ( G NeighbVtx A ) /\ C e. ( G NeighbVtx A ) ) /\ ( C e. ( G NeighbVtx B ) /\ A e. ( G NeighbVtx B ) ) /\ ( A e. ( G NeighbVtx C ) /\ B e. ( G NeighbVtx C ) ) ) <-> ( ( B e. ( G NeighbVtx A ) /\ C e. ( G NeighbVtx B ) /\ A e. ( G NeighbVtx C ) ) /\ ( C e. ( G NeighbVtx A ) /\ A e. ( G NeighbVtx B ) /\ B e. ( G NeighbVtx C ) ) ) ) )
75 nbgrsym 
 |-  ( B e. ( G NeighbVtx A ) <-> A e. ( G NeighbVtx B ) )
76 nbgrsym 
 |-  ( C e. ( G NeighbVtx B ) <-> B e. ( G NeighbVtx C ) )
77 nbgrsym 
 |-  ( A e. ( G NeighbVtx C ) <-> C e. ( G NeighbVtx A ) )
78 75 76 77 3anbi123i 
 |-  ( ( B e. ( G NeighbVtx A ) /\ C e. ( G NeighbVtx B ) /\ A e. ( G NeighbVtx C ) ) <-> ( A e. ( G NeighbVtx B ) /\ B e. ( G NeighbVtx C ) /\ C e. ( G NeighbVtx A ) ) )
79 78 a1i 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( B e. ( G NeighbVtx A ) /\ C e. ( G NeighbVtx B ) /\ A e. ( G NeighbVtx C ) ) <-> ( A e. ( G NeighbVtx B ) /\ B e. ( G NeighbVtx C ) /\ C e. ( G NeighbVtx A ) ) ) )
80 79 anbi1d 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( ( B e. ( G NeighbVtx A ) /\ C e. ( G NeighbVtx B ) /\ A e. ( G NeighbVtx C ) ) /\ ( C e. ( G NeighbVtx A ) /\ A e. ( G NeighbVtx B ) /\ B e. ( G NeighbVtx C ) ) ) <-> ( ( A e. ( G NeighbVtx B ) /\ B e. ( G NeighbVtx C ) /\ C e. ( G NeighbVtx A ) ) /\ ( C e. ( G NeighbVtx A ) /\ A e. ( G NeighbVtx B ) /\ B e. ( G NeighbVtx C ) ) ) ) )
81 3anrot 
 |-  ( ( C e. ( G NeighbVtx A ) /\ A e. ( G NeighbVtx B ) /\ B e. ( G NeighbVtx C ) ) <-> ( A e. ( G NeighbVtx B ) /\ B e. ( G NeighbVtx C ) /\ C e. ( G NeighbVtx A ) ) )
82 81 bicomi 
 |-  ( ( A e. ( G NeighbVtx B ) /\ B e. ( G NeighbVtx C ) /\ C e. ( G NeighbVtx A ) ) <-> ( C e. ( G NeighbVtx A ) /\ A e. ( G NeighbVtx B ) /\ B e. ( G NeighbVtx C ) ) )
83 82 anbi1i 
 |-  ( ( ( A e. ( G NeighbVtx B ) /\ B e. ( G NeighbVtx C ) /\ C e. ( G NeighbVtx A ) ) /\ ( C e. ( G NeighbVtx A ) /\ A e. ( G NeighbVtx B ) /\ B e. ( G NeighbVtx C ) ) ) <-> ( ( C e. ( G NeighbVtx A ) /\ A e. ( G NeighbVtx B ) /\ B e. ( G NeighbVtx C ) ) /\ ( C e. ( G NeighbVtx A ) /\ A e. ( G NeighbVtx B ) /\ B e. ( G NeighbVtx C ) ) ) )
84 anidm 
 |-  ( ( ( C e. ( G NeighbVtx A ) /\ A e. ( G NeighbVtx B ) /\ B e. ( G NeighbVtx C ) ) /\ ( C e. ( G NeighbVtx A ) /\ A e. ( G NeighbVtx B ) /\ B e. ( G NeighbVtx C ) ) ) <-> ( C e. ( G NeighbVtx A ) /\ A e. ( G NeighbVtx B ) /\ B e. ( G NeighbVtx C ) ) )
85 83 84 bitri 
 |-  ( ( ( A e. ( G NeighbVtx B ) /\ B e. ( G NeighbVtx C ) /\ C e. ( G NeighbVtx A ) ) /\ ( C e. ( G NeighbVtx A ) /\ A e. ( G NeighbVtx B ) /\ B e. ( G NeighbVtx C ) ) ) <-> ( C e. ( G NeighbVtx A ) /\ A e. ( G NeighbVtx B ) /\ B e. ( G NeighbVtx C ) ) )
86 85 a1i 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( ( A e. ( G NeighbVtx B ) /\ B e. ( G NeighbVtx C ) /\ C e. ( G NeighbVtx A ) ) /\ ( C e. ( G NeighbVtx A ) /\ A e. ( G NeighbVtx B ) /\ B e. ( G NeighbVtx C ) ) ) <-> ( C e. ( G NeighbVtx A ) /\ A e. ( G NeighbVtx B ) /\ B e. ( G NeighbVtx C ) ) ) )
87 tpid1g 
 |-  ( A e. X -> A e. { A , B , C } )
88 tpid2g 
 |-  ( B e. Y -> B e. { A , B , C } )
89 tpid3g 
 |-  ( C e. Z -> C e. { A , B , C } )
90 87 88 89 3anim123i 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( A e. { A , B , C } /\ B e. { A , B , C } /\ C e. { A , B , C } ) )
91 df-3an 
 |-  ( ( A e. { A , B , C } /\ B e. { A , B , C } /\ C e. { A , B , C } ) <-> ( ( A e. { A , B , C } /\ B e. { A , B , C } ) /\ C e. { A , B , C } ) )
92 90 91 sylib 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( ( A e. { A , B , C } /\ B e. { A , B , C } ) /\ C e. { A , B , C } ) )
93 simplr 
 |-  ( ( ( A e. { A , B , C } /\ B e. { A , B , C } ) /\ C e. { A , B , C } ) -> B e. { A , B , C } )
94 93 anim1ci 
 |-  ( ( ( ( A e. { A , B , C } /\ B e. { A , B , C } ) /\ C e. { A , B , C } ) /\ G e. UPGraph ) -> ( G e. UPGraph /\ B e. { A , B , C } ) )
95 94 3adant3 
 |-  ( ( ( ( A e. { A , B , C } /\ B e. { A , B , C } ) /\ C e. { A , B , C } ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( G e. UPGraph /\ B e. { A , B , C } ) )
96 simpll 
 |-  ( ( ( A e. { A , B , C } /\ B e. { A , B , C } ) /\ C e. { A , B , C } ) -> A e. { A , B , C } )
97 simp1 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> A =/= B )
98 96 97 anim12i 
 |-  ( ( ( ( A e. { A , B , C } /\ B e. { A , B , C } ) /\ C e. { A , B , C } ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( A e. { A , B , C } /\ A =/= B ) )
99 3 1 nbupgrel 
 |-  ( ( ( G e. UPGraph /\ B e. { A , B , C } ) /\ ( A e. { A , B , C } /\ A =/= B ) ) -> ( A e. ( G NeighbVtx B ) <-> { A , B } e. E ) )
100 95 98 99 3imp3i2an 
 |-  ( ( ( ( A e. { A , B , C } /\ B e. { A , B , C } ) /\ C e. { A , B , C } ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( A e. ( G NeighbVtx B ) <-> { A , B } e. E ) )
101 simpr 
 |-  ( ( ( A e. { A , B , C } /\ B e. { A , B , C } ) /\ C e. { A , B , C } ) -> C e. { A , B , C } )
102 101 anim1ci 
 |-  ( ( ( ( A e. { A , B , C } /\ B e. { A , B , C } ) /\ C e. { A , B , C } ) /\ G e. UPGraph ) -> ( G e. UPGraph /\ C e. { A , B , C } ) )
103 102 3adant3 
 |-  ( ( ( ( A e. { A , B , C } /\ B e. { A , B , C } ) /\ C e. { A , B , C } ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( G e. UPGraph /\ C e. { A , B , C } ) )
104 simp3 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> B =/= C )
105 93 104 anim12i 
 |-  ( ( ( ( A e. { A , B , C } /\ B e. { A , B , C } ) /\ C e. { A , B , C } ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( B e. { A , B , C } /\ B =/= C ) )
106 3 1 nbupgrel 
 |-  ( ( ( G e. UPGraph /\ C e. { A , B , C } ) /\ ( B e. { A , B , C } /\ B =/= C ) ) -> ( B e. ( G NeighbVtx C ) <-> { B , C } e. E ) )
107 103 105 106 3imp3i2an 
 |-  ( ( ( ( A e. { A , B , C } /\ B e. { A , B , C } ) /\ C e. { A , B , C } ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( B e. ( G NeighbVtx C ) <-> { B , C } e. E ) )
108 96 anim1ci 
 |-  ( ( ( ( A e. { A , B , C } /\ B e. { A , B , C } ) /\ C e. { A , B , C } ) /\ G e. UPGraph ) -> ( G e. UPGraph /\ A e. { A , B , C } ) )
109 108 3adant3 
 |-  ( ( ( ( A e. { A , B , C } /\ B e. { A , B , C } ) /\ C e. { A , B , C } ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( G e. UPGraph /\ A e. { 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 e. { A , B , C } /\ B e. { A , B , C } ) /\ C e. { A , B , C } ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( C e. { A , B , C } /\ C =/= A ) )
113 3 1 nbupgrel 
 |-  ( ( ( G e. UPGraph /\ A e. { A , B , C } ) /\ ( C e. { A , B , C } /\ C =/= A ) ) -> ( C e. ( G NeighbVtx A ) <-> { C , A } e. E ) )
114 109 112 113 3imp3i2an 
 |-  ( ( ( ( A e. { A , B , C } /\ B e. { A , B , C } ) /\ C e. { A , B , C } ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( C e. ( G NeighbVtx A ) <-> { C , A } e. E ) )
115 100 107 114 3anbi123d 
 |-  ( ( ( ( A e. { A , B , C } /\ B e. { A , B , C } ) /\ C e. { A , B , C } ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( A e. ( G NeighbVtx B ) /\ B e. ( G NeighbVtx C ) /\ C e. ( G NeighbVtx A ) ) <-> ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) )
116 92 115 syl3an1 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( A e. ( G NeighbVtx B ) /\ B e. ( G NeighbVtx C ) /\ C e. ( G NeighbVtx A ) ) <-> ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) )
117 81 116 bitrid 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( C e. ( G NeighbVtx A ) /\ A e. ( G NeighbVtx B ) /\ B e. ( G NeighbVtx C ) ) <-> ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) )
118 80 86 117 3bitrd 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( ( B e. ( G NeighbVtx A ) /\ C e. ( G NeighbVtx B ) /\ A e. ( G NeighbVtx C ) ) /\ ( C e. ( G NeighbVtx A ) /\ A e. ( G NeighbVtx B ) /\ B e. ( G NeighbVtx C ) ) ) <-> ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) )
119 72 74 118 3bitrd 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( A. n e. { B , C } n e. ( G NeighbVtx A ) /\ A. n e. { C , A } n e. ( G NeighbVtx B ) /\ A. n e. { A , B } n e. ( G NeighbVtx C ) ) <-> ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) )
120 5 57 119 3bitrd 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( G e. ComplGraph <-> ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) )