This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nb3grprlem2

Description: Lemma 2 for nb3grpr . (Contributed by Alexander van der Vekens, 17-Oct-2017) (Revised by AV, 28-Oct-2020) (Proof shortened by AV, 13-Feb-2022)

Ref Expression
Hypotheses nb3grpr.v 
|- V = ( Vtx ` G )
nb3grpr.e 
|- E = ( Edg ` G )
nb3grpr.g 
|- ( ph -> G e. USGraph )
nb3grpr.t 
|- ( ph -> V = { A , B , C } )
nb3grpr.s 
|- ( ph -> ( A e. X /\ B e. Y /\ C e. Z ) )
nb3grpr.n 
|- ( ph -> ( A =/= B /\ A =/= C /\ B =/= C ) )
Assertion nb3grprlem2 
|- ( ph -> ( ( G NeighbVtx A ) = { B , C } <-> E. v e. V E. w e. ( V \ { v } ) ( G NeighbVtx A ) = { v , w } ) )

Proof

Step Hyp Ref Expression
1 nb3grpr.v 
 |-  V = ( Vtx ` G )
2 nb3grpr.e 
 |-  E = ( Edg ` G )
3 nb3grpr.g 
 |-  ( ph -> G e. USGraph )
4 nb3grpr.t 
 |-  ( ph -> V = { A , B , C } )
5 nb3grpr.s 
 |-  ( ph -> ( A e. X /\ B e. Y /\ C e. Z ) )
6 nb3grpr.n 
 |-  ( ph -> ( A =/= B /\ A =/= C /\ B =/= C ) )
7 sneq 
 |-  ( v = A -> { v } = { A } )
8 7 difeq2d 
 |-  ( v = A -> ( { A , B , C } \ { v } ) = ( { A , B , C } \ { A } ) )
9 preq1 
 |-  ( v = A -> { v , w } = { A , w } )
10 9 eqeq2d 
 |-  ( v = A -> ( ( G NeighbVtx A ) = { v , w } <-> ( G NeighbVtx A ) = { A , w } ) )
11 8 10 rexeqbidv 
 |-  ( v = A -> ( E. w e. ( { A , B , C } \ { v } ) ( G NeighbVtx A ) = { v , w } <-> E. w e. ( { A , B , C } \ { A } ) ( G NeighbVtx A ) = { A , w } ) )
12 sneq 
 |-  ( v = B -> { v } = { B } )
13 12 difeq2d 
 |-  ( v = B -> ( { A , B , C } \ { v } ) = ( { A , B , C } \ { B } ) )
14 preq1 
 |-  ( v = B -> { v , w } = { B , w } )
15 14 eqeq2d 
 |-  ( v = B -> ( ( G NeighbVtx A ) = { v , w } <-> ( G NeighbVtx A ) = { B , w } ) )
16 13 15 rexeqbidv 
 |-  ( v = B -> ( E. w e. ( { A , B , C } \ { v } ) ( G NeighbVtx A ) = { v , w } <-> E. w e. ( { A , B , C } \ { B } ) ( G NeighbVtx A ) = { B , w } ) )
17 sneq 
 |-  ( v = C -> { v } = { C } )
18 17 difeq2d 
 |-  ( v = C -> ( { A , B , C } \ { v } ) = ( { A , B , C } \ { C } ) )
19 preq1 
 |-  ( v = C -> { v , w } = { C , w } )
20 19 eqeq2d 
 |-  ( v = C -> ( ( G NeighbVtx A ) = { v , w } <-> ( G NeighbVtx A ) = { C , w } ) )
21 18 20 rexeqbidv 
 |-  ( v = C -> ( E. w e. ( { A , B , C } \ { v } ) ( G NeighbVtx A ) = { v , w } <-> E. w e. ( { A , B , C } \ { C } ) ( G NeighbVtx A ) = { C , w } ) )
22 11 16 21 rextpg 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( E. v e. { A , B , C } E. w e. ( { A , B , C } \ { v } ) ( G NeighbVtx A ) = { v , w } <-> ( E. w e. ( { A , B , C } \ { A } ) ( G NeighbVtx A ) = { A , w } \/ E. w e. ( { A , B , C } \ { B } ) ( G NeighbVtx A ) = { B , w } \/ E. w e. ( { A , B , C } \ { C } ) ( G NeighbVtx A ) = { C , w } ) ) )
23 5 22 syl 
 |-  ( ph -> ( E. v e. { A , B , C } E. w e. ( { A , B , C } \ { v } ) ( G NeighbVtx A ) = { v , w } <-> ( E. w e. ( { A , B , C } \ { A } ) ( G NeighbVtx A ) = { A , w } \/ E. w e. ( { A , B , C } \ { B } ) ( G NeighbVtx A ) = { B , w } \/ E. w e. ( { A , B , C } \ { C } ) ( G NeighbVtx A ) = { C , w } ) ) )
24 4 3 jca 
 |-  ( ph -> ( V = { A , B , C } /\ G e. USGraph ) )
25 simpl 
 |-  ( ( V = { A , B , C } /\ G e. USGraph ) -> V = { A , B , C } )
26 difeq1 
 |-  ( V = { A , B , C } -> ( V \ { v } ) = ( { A , B , C } \ { v } ) )
27 26 adantr 
 |-  ( ( V = { A , B , C } /\ G e. USGraph ) -> ( V \ { v } ) = ( { A , B , C } \ { v } ) )
28 27 rexeqdv 
 |-  ( ( V = { A , B , C } /\ G e. USGraph ) -> ( E. w e. ( V \ { v } ) ( G NeighbVtx A ) = { v , w } <-> E. w e. ( { A , B , C } \ { v } ) ( G NeighbVtx A ) = { v , w } ) )
29 25 28 rexeqbidv 
 |-  ( ( V = { A , B , C } /\ G e. USGraph ) -> ( E. v e. V E. w e. ( V \ { v } ) ( G NeighbVtx A ) = { v , w } <-> E. v e. { A , B , C } E. w e. ( { A , B , C } \ { v } ) ( G NeighbVtx A ) = { v , w } ) )
30 24 29 syl 
 |-  ( ph -> ( E. v e. V E. w e. ( V \ { v } ) ( G NeighbVtx A ) = { v , w } <-> E. v e. { A , B , C } E. w e. ( { A , B , C } \ { v } ) ( G NeighbVtx A ) = { v , w } ) )
31 preq2 
 |-  ( w = B -> { A , w } = { A , B } )
32 31 eqeq2d 
 |-  ( w = B -> ( ( G NeighbVtx A ) = { A , w } <-> ( G NeighbVtx A ) = { A , B } ) )
33 preq2 
 |-  ( w = C -> { A , w } = { A , C } )
34 33 eqeq2d 
 |-  ( w = C -> ( ( G NeighbVtx A ) = { A , w } <-> ( G NeighbVtx A ) = { A , C } ) )
35 32 34 rexprg 
 |-  ( ( B e. Y /\ C e. Z ) -> ( E. w e. { B , C } ( G NeighbVtx A ) = { A , w } <-> ( ( G NeighbVtx A ) = { A , B } \/ ( G NeighbVtx A ) = { A , C } ) ) )
36 35 3adant1 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( E. w e. { B , C } ( G NeighbVtx A ) = { A , w } <-> ( ( G NeighbVtx A ) = { A , B } \/ ( G NeighbVtx A ) = { A , C } ) ) )
37 preq2 
 |-  ( w = C -> { B , w } = { B , C } )
38 37 eqeq2d 
 |-  ( w = C -> ( ( G NeighbVtx A ) = { B , w } <-> ( G NeighbVtx A ) = { B , C } ) )
39 preq2 
 |-  ( w = A -> { B , w } = { B , A } )
40 39 eqeq2d 
 |-  ( w = A -> ( ( G NeighbVtx A ) = { B , w } <-> ( G NeighbVtx A ) = { B , A } ) )
41 38 40 rexprg 
 |-  ( ( C e. Z /\ A e. X ) -> ( E. w e. { C , A } ( G NeighbVtx A ) = { B , w } <-> ( ( G NeighbVtx A ) = { B , C } \/ ( G NeighbVtx A ) = { B , A } ) ) )
42 41 ancoms 
 |-  ( ( A e. X /\ C e. Z ) -> ( E. w e. { C , A } ( G NeighbVtx A ) = { B , w } <-> ( ( G NeighbVtx A ) = { B , C } \/ ( G NeighbVtx A ) = { B , A } ) ) )
43 42 3adant2 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( E. w e. { C , A } ( G NeighbVtx A ) = { B , w } <-> ( ( G NeighbVtx A ) = { B , C } \/ ( G NeighbVtx A ) = { B , A } ) ) )
44 preq2 
 |-  ( w = A -> { C , w } = { C , A } )
45 44 eqeq2d 
 |-  ( w = A -> ( ( G NeighbVtx A ) = { C , w } <-> ( G NeighbVtx A ) = { C , A } ) )
46 preq2 
 |-  ( w = B -> { C , w } = { C , B } )
47 46 eqeq2d 
 |-  ( w = B -> ( ( G NeighbVtx A ) = { C , w } <-> ( G NeighbVtx A ) = { C , B } ) )
48 45 47 rexprg 
 |-  ( ( A e. X /\ B e. Y ) -> ( E. w e. { A , B } ( G NeighbVtx A ) = { C , w } <-> ( ( G NeighbVtx A ) = { C , A } \/ ( G NeighbVtx A ) = { C , B } ) ) )
49 48 3adant3 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( E. w e. { A , B } ( G NeighbVtx A ) = { C , w } <-> ( ( G NeighbVtx A ) = { C , A } \/ ( G NeighbVtx A ) = { C , B } ) ) )
50 36 43 49 3orbi123d 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( ( E. w e. { B , C } ( G NeighbVtx A ) = { A , w } \/ E. w e. { C , A } ( G NeighbVtx A ) = { B , w } \/ E. w e. { A , B } ( G NeighbVtx A ) = { C , w } ) <-> ( ( ( G NeighbVtx A ) = { A , B } \/ ( G NeighbVtx A ) = { A , C } ) \/ ( ( G NeighbVtx A ) = { B , C } \/ ( G NeighbVtx A ) = { B , A } ) \/ ( ( G NeighbVtx A ) = { C , A } \/ ( G NeighbVtx A ) = { C , B } ) ) ) )
51 5 50 syl 
 |-  ( ph -> ( ( E. w e. { B , C } ( G NeighbVtx A ) = { A , w } \/ E. w e. { C , A } ( G NeighbVtx A ) = { B , w } \/ E. w e. { A , B } ( G NeighbVtx A ) = { C , w } ) <-> ( ( ( G NeighbVtx A ) = { A , B } \/ ( G NeighbVtx A ) = { A , C } ) \/ ( ( G NeighbVtx A ) = { B , C } \/ ( G NeighbVtx A ) = { B , A } ) \/ ( ( G NeighbVtx A ) = { C , A } \/ ( G NeighbVtx A ) = { C , B } ) ) ) )
52 tprot 
 |-  { A , B , C } = { B , C , A }
53 52 a1i 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> { A , B , C } = { B , C , A } )
54 53 difeq1d 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { A } ) = ( { B , C , A } \ { A } ) )
55 necom 
 |-  ( A =/= B <-> B =/= A )
56 necom 
 |-  ( A =/= C <-> C =/= A )
57 diftpsn3 
 |-  ( ( B =/= A /\ C =/= A ) -> ( { B , C , A } \ { A } ) = { B , C } )
58 55 56 57 syl2anb 
 |-  ( ( A =/= B /\ A =/= C ) -> ( { B , C , A } \ { A } ) = { B , C } )
59 58 3adant3 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { B , C , A } \ { A } ) = { B , C } )
60 54 59 eqtrd 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { A } ) = { B , C } )
61 60 rexeqdv 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( E. w e. ( { A , B , C } \ { A } ) ( G NeighbVtx A ) = { A , w } <-> E. w e. { B , C } ( G NeighbVtx A ) = { A , w } ) )
62 tprot 
 |-  { C , A , B } = { A , B , C }
63 62 eqcomi 
 |-  { A , B , C } = { C , A , B }
64 63 a1i 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> { A , B , C } = { C , A , B } )
65 64 difeq1d 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { B } ) = ( { C , A , B } \ { B } ) )
66 necom 
 |-  ( B =/= C <-> C =/= B )
67 66 anbi1i 
 |-  ( ( B =/= C /\ A =/= B ) <-> ( C =/= B /\ A =/= B ) )
68 67 biimpi 
 |-  ( ( B =/= C /\ A =/= B ) -> ( C =/= B /\ A =/= B ) )
69 68 ancoms 
 |-  ( ( A =/= B /\ B =/= C ) -> ( C =/= B /\ A =/= B ) )
70 diftpsn3 
 |-  ( ( C =/= B /\ A =/= B ) -> ( { C , A , B } \ { B } ) = { C , A } )
71 69 70 syl 
 |-  ( ( A =/= B /\ B =/= C ) -> ( { C , A , B } \ { B } ) = { C , A } )
72 71 3adant2 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { C , A , B } \ { B } ) = { C , A } )
73 65 72 eqtrd 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { B } ) = { C , A } )
74 73 rexeqdv 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( E. w e. ( { A , B , C } \ { B } ) ( G NeighbVtx A ) = { B , w } <-> E. w e. { C , A } ( G NeighbVtx A ) = { B , w } ) )
75 diftpsn3 
 |-  ( ( A =/= C /\ B =/= C ) -> ( { A , B , C } \ { C } ) = { A , B } )
76 75 3adant1 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { C } ) = { A , B } )
77 76 rexeqdv 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( E. w e. ( { A , B , C } \ { C } ) ( G NeighbVtx A ) = { C , w } <-> E. w e. { A , B } ( G NeighbVtx A ) = { C , w } ) )
78 61 74 77 3orbi123d 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( ( E. w e. ( { A , B , C } \ { A } ) ( G NeighbVtx A ) = { A , w } \/ E. w e. ( { A , B , C } \ { B } ) ( G NeighbVtx A ) = { B , w } \/ E. w e. ( { A , B , C } \ { C } ) ( G NeighbVtx A ) = { C , w } ) <-> ( E. w e. { B , C } ( G NeighbVtx A ) = { A , w } \/ E. w e. { C , A } ( G NeighbVtx A ) = { B , w } \/ E. w e. { A , B } ( G NeighbVtx A ) = { C , w } ) ) )
79 6 78 syl 
 |-  ( ph -> ( ( E. w e. ( { A , B , C } \ { A } ) ( G NeighbVtx A ) = { A , w } \/ E. w e. ( { A , B , C } \ { B } ) ( G NeighbVtx A ) = { B , w } \/ E. w e. ( { A , B , C } \ { C } ) ( G NeighbVtx A ) = { C , w } ) <-> ( E. w e. { B , C } ( G NeighbVtx A ) = { A , w } \/ E. w e. { C , A } ( G NeighbVtx A ) = { B , w } \/ E. w e. { A , B } ( G NeighbVtx A ) = { C , w } ) ) )
80 prcom 
 |-  { C , B } = { B , C }
81 80 eqeq2i 
 |-  ( ( G NeighbVtx A ) = { C , B } <-> ( G NeighbVtx A ) = { B , C } )
82 81 orbi2i 
 |-  ( ( ( G NeighbVtx A ) = { B , C } \/ ( G NeighbVtx A ) = { C , B } ) <-> ( ( G NeighbVtx A ) = { B , C } \/ ( G NeighbVtx A ) = { B , C } ) )
83 oridm 
 |-  ( ( ( G NeighbVtx A ) = { B , C } \/ ( G NeighbVtx A ) = { B , C } ) <-> ( G NeighbVtx A ) = { B , C } )
84 82 83 bitr2i 
 |-  ( ( G NeighbVtx A ) = { B , C } <-> ( ( G NeighbVtx A ) = { B , C } \/ ( G NeighbVtx A ) = { C , B } ) )
85 84 a1i 
 |-  ( ph -> ( ( G NeighbVtx A ) = { B , C } <-> ( ( G NeighbVtx A ) = { B , C } \/ ( G NeighbVtx A ) = { C , B } ) ) )
86 nbgrnself2 
 |-  A e/ ( G NeighbVtx A )
87 df-nel 
 |-  ( A e/ ( G NeighbVtx A ) <-> -. A e. ( G NeighbVtx A ) )
88 prid2g 
 |-  ( A e. X -> A e. { B , A } )
89 88 3ad2ant1 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> A e. { B , A } )
90 eleq2 
 |-  ( ( G NeighbVtx A ) = { B , A } -> ( A e. ( G NeighbVtx A ) <-> A e. { B , A } ) )
91 89 90 syl5ibrcom 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( ( G NeighbVtx A ) = { B , A } -> A e. ( G NeighbVtx A ) ) )
92 91 con3rr3 
 |-  ( -. A e. ( G NeighbVtx A ) -> ( ( A e. X /\ B e. Y /\ C e. Z ) -> -. ( G NeighbVtx A ) = { B , A } ) )
93 87 92 sylbi 
 |-  ( A e/ ( G NeighbVtx A ) -> ( ( A e. X /\ B e. Y /\ C e. Z ) -> -. ( G NeighbVtx A ) = { B , A } ) )
94 86 5 93 mpsyl 
 |-  ( ph -> -. ( G NeighbVtx A ) = { B , A } )
95 biorf 
 |-  ( -. ( G NeighbVtx A ) = { B , A } -> ( ( G NeighbVtx A ) = { B , C } <-> ( ( G NeighbVtx A ) = { B , A } \/ ( G NeighbVtx A ) = { B , C } ) ) )
96 orcom 
 |-  ( ( ( G NeighbVtx A ) = { B , A } \/ ( G NeighbVtx A ) = { B , C } ) <-> ( ( G NeighbVtx A ) = { B , C } \/ ( G NeighbVtx A ) = { B , A } ) )
97 95 96 bitrdi 
 |-  ( -. ( G NeighbVtx A ) = { B , A } -> ( ( G NeighbVtx A ) = { B , C } <-> ( ( G NeighbVtx A ) = { B , C } \/ ( G NeighbVtx A ) = { B , A } ) ) )
98 94 97 syl 
 |-  ( ph -> ( ( G NeighbVtx A ) = { B , C } <-> ( ( G NeighbVtx A ) = { B , C } \/ ( G NeighbVtx A ) = { B , A } ) ) )
99 prid2g 
 |-  ( A e. X -> A e. { C , A } )
100 99 3ad2ant1 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> A e. { C , A } )
101 eleq2 
 |-  ( ( G NeighbVtx A ) = { C , A } -> ( A e. ( G NeighbVtx A ) <-> A e. { C , A } ) )
102 100 101 syl5ibrcom 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( ( G NeighbVtx A ) = { C , A } -> A e. ( G NeighbVtx A ) ) )
103 102 con3rr3 
 |-  ( -. A e. ( G NeighbVtx A ) -> ( ( A e. X /\ B e. Y /\ C e. Z ) -> -. ( G NeighbVtx A ) = { C , A } ) )
104 87 103 sylbi 
 |-  ( A e/ ( G NeighbVtx A ) -> ( ( A e. X /\ B e. Y /\ C e. Z ) -> -. ( G NeighbVtx A ) = { C , A } ) )
105 86 5 104 mpsyl 
 |-  ( ph -> -. ( G NeighbVtx A ) = { C , A } )
106 biorf 
 |-  ( -. ( G NeighbVtx A ) = { C , A } -> ( ( G NeighbVtx A ) = { C , B } <-> ( ( G NeighbVtx A ) = { C , A } \/ ( G NeighbVtx A ) = { C , B } ) ) )
107 105 106 syl 
 |-  ( ph -> ( ( G NeighbVtx A ) = { C , B } <-> ( ( G NeighbVtx A ) = { C , A } \/ ( G NeighbVtx A ) = { C , B } ) ) )
108 98 107 orbi12d 
 |-  ( ph -> ( ( ( G NeighbVtx A ) = { B , C } \/ ( G NeighbVtx A ) = { C , B } ) <-> ( ( ( G NeighbVtx A ) = { B , C } \/ ( G NeighbVtx A ) = { B , A } ) \/ ( ( G NeighbVtx A ) = { C , A } \/ ( G NeighbVtx A ) = { C , B } ) ) ) )
109 prid1g 
 |-  ( A e. X -> A e. { A , B } )
110 109 3ad2ant1 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> A e. { A , B } )
111 eleq2 
 |-  ( ( G NeighbVtx A ) = { A , B } -> ( A e. ( G NeighbVtx A ) <-> A e. { A , B } ) )
112 110 111 syl5ibrcom 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( ( G NeighbVtx A ) = { A , B } -> A e. ( G NeighbVtx A ) ) )
113 112 con3dimp 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ -. A e. ( G NeighbVtx A ) ) -> -. ( G NeighbVtx A ) = { A , B } )
114 prid1g 
 |-  ( A e. X -> A e. { A , C } )
115 114 3ad2ant1 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> A e. { A , C } )
116 eleq2 
 |-  ( ( G NeighbVtx A ) = { A , C } -> ( A e. ( G NeighbVtx A ) <-> A e. { A , C } ) )
117 115 116 syl5ibrcom 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( ( G NeighbVtx A ) = { A , C } -> A e. ( G NeighbVtx A ) ) )
118 117 con3dimp 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ -. A e. ( G NeighbVtx A ) ) -> -. ( G NeighbVtx A ) = { A , C } )
119 113 118 jca 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ -. A e. ( G NeighbVtx A ) ) -> ( -. ( G NeighbVtx A ) = { A , B } /\ -. ( G NeighbVtx A ) = { A , C } ) )
120 119 expcom 
 |-  ( -. A e. ( G NeighbVtx A ) -> ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( -. ( G NeighbVtx A ) = { A , B } /\ -. ( G NeighbVtx A ) = { A , C } ) ) )
121 87 120 sylbi 
 |-  ( A e/ ( G NeighbVtx A ) -> ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( -. ( G NeighbVtx A ) = { A , B } /\ -. ( G NeighbVtx A ) = { A , C } ) ) )
122 86 5 121 mpsyl 
 |-  ( ph -> ( -. ( G NeighbVtx A ) = { A , B } /\ -. ( G NeighbVtx A ) = { A , C } ) )
123 ioran 
 |-  ( -. ( ( G NeighbVtx A ) = { A , B } \/ ( G NeighbVtx A ) = { A , C } ) <-> ( -. ( G NeighbVtx A ) = { A , B } /\ -. ( G NeighbVtx A ) = { A , C } ) )
124 122 123 sylibr 
 |-  ( ph -> -. ( ( G NeighbVtx A ) = { A , B } \/ ( G NeighbVtx A ) = { A , C } ) )
125 124 3bior1fd 
 |-  ( ph -> ( ( ( ( G NeighbVtx A ) = { B , C } \/ ( G NeighbVtx A ) = { B , A } ) \/ ( ( G NeighbVtx A ) = { C , A } \/ ( G NeighbVtx A ) = { C , B } ) ) <-> ( ( ( G NeighbVtx A ) = { A , B } \/ ( G NeighbVtx A ) = { A , C } ) \/ ( ( G NeighbVtx A ) = { B , C } \/ ( G NeighbVtx A ) = { B , A } ) \/ ( ( G NeighbVtx A ) = { C , A } \/ ( G NeighbVtx A ) = { C , B } ) ) ) )
126 85 108 125 3bitrd 
 |-  ( ph -> ( ( G NeighbVtx A ) = { B , C } <-> ( ( ( G NeighbVtx A ) = { A , B } \/ ( G NeighbVtx A ) = { A , C } ) \/ ( ( G NeighbVtx A ) = { B , C } \/ ( G NeighbVtx A ) = { B , A } ) \/ ( ( G NeighbVtx A ) = { C , A } \/ ( G NeighbVtx A ) = { C , B } ) ) ) )
127 51 79 126 3bitr4rd 
 |-  ( ph -> ( ( G NeighbVtx A ) = { B , C } <-> ( E. w e. ( { A , B , C } \ { A } ) ( G NeighbVtx A ) = { A , w } \/ E. w e. ( { A , B , C } \ { B } ) ( G NeighbVtx A ) = { B , w } \/ E. w e. ( { A , B , C } \ { C } ) ( G NeighbVtx A ) = { C , w } ) ) )
128 23 30 127 3bitr4rd 
 |-  ( ph -> ( ( G NeighbVtx A ) = { B , C } <-> E. v e. V E. w e. ( V \ { v } ) ( G NeighbVtx A ) = { v , w } ) )