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 ⊢ 𝐸 = ( Edg ‘ 𝐺 )
cplgr3v.t ⊢ ( Vtx ‘ 𝐺 ) = { 𝐴 , 𝐵 , 𝐶 }
Assertion cplgr3v ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ 𝐺 ∈ UPGraph ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( 𝐺 ∈ ComplGraph ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) )

Proof

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