Theorem nb3grprlem2 26283

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

Hypotheses

Ref	Expression
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

Ref	Expression
nb3grprlem2	|- ( ph -> ( ( G NeighbVtx A ) = { B , C } <-> E. v e. V E. w e. ( V \ { v } ) ( G NeighbVtx A ) = { v , w } ) )

Distinct variable groups:   v, A   v, B   v, C   v, E   v, G   v, V   ph, v   w, A, v   w, B   w, C   w, G   w, V

Allowed substitution hints:   ph( w)   E( w)   X( w, v)   Y( w, v)   Z( w, v)

Proof of Theorem nb3grprlem2

Step	Hyp	Ref	Expression
1		nb3grpr.s	. . 3 |- ( ph -> ( A e. X /\ B e. Y /\ C e. Z ) )
2		sneq 4187	. . . . . 6 |- ( v = A -> { v } = { A } )
3	2	difeq2d 3728	. . . . 5 |- ( v = A -> ( { A , B , C } \ { v } ) = ( { A , B , C } \ { A } ) )
4		preq1 4268	. . . . . 6 |- ( v = A -> { v , w } = { A , w } )
5	4	eqeq2d 2632	. . . . 5 |- ( v = A -> ( ( G NeighbVtx A ) = { v , w } <-> ( G NeighbVtx A ) = { A , w } ) )
6	3, 5	rexeqbidv 3153	. . . 4 |- ( 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 } ) )
7		sneq 4187	. . . . . 6 |- ( v = B -> { v } = { B } )
8	7	difeq2d 3728	. . . . 5 |- ( v = B -> ( { A , B , C } \ { v } ) = ( { A , B , C } \ { B } ) )
9		preq1 4268	. . . . . 6 |- ( v = B -> { v , w } = { B , w } )
10	9	eqeq2d 2632	. . . . 5 |- ( v = B -> ( ( G NeighbVtx A ) = { v , w } <-> ( G NeighbVtx A ) = { B , w } ) )
11	8, 10	rexeqbidv 3153	. . . 4 |- ( 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 } ) )
12		sneq 4187	. . . . . 6 |- ( v = C -> { v } = { C } )
13	12	difeq2d 3728	. . . . 5 |- ( v = C -> ( { A , B , C } \ { v } ) = ( { A , B , C } \ { C } ) )
14		preq1 4268	. . . . . 6 |- ( v = C -> { v , w } = { C , w } )
15	14	eqeq2d 2632	. . . . 5 |- ( v = C -> ( ( G NeighbVtx A ) = { v , w } <-> ( G NeighbVtx A ) = { C , w } ) )
16	13, 15	rexeqbidv 3153	. . . 4 |- ( 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 } ) )
17	6, 11, 16	rextpg 4237	. . 3 |- ( ( 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 } ) ) )
18	1, 17	syl 17	. 2 |- ( 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 } ) ) )
19		nb3grpr.t	. . . 4 |- ( ph -> V = { A , B , C } )
20		nb3grpr.g	. . . 4 |- ( ph -> G e. USGraph )
21	19, 20	jca 554	. . 3 |- ( ph -> ( V = { A , B , C } /\ G e. USGraph ) )
22		simpl 473	. . . 4 |- ( ( V = { A , B , C } /\ G e. USGraph ) -> V = { A , B , C } )
23		difeq1 3721	. . . . . 6 |- ( V = { A , B , C } -> ( V \ { v } ) = ( { A , B , C } \ { v } ) )
24	23	adantr 481	. . . . 5 |- ( ( V = { A , B , C } /\ G e. USGraph ) -> ( V \ { v } ) = ( { A , B , C } \ { v } ) )
25	24	rexeqdv 3145	. . . 4 |- ( ( 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 } ) )
26	22, 25	rexeqbidv 3153	. . 3 |- ( ( 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 } ) )
27	21, 26	syl 17	. 2 |- ( 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 } ) )
28		preq2 4269	. . . . . . . 8 |- ( w = B -> { A , w } = { A , B } )
29	28	eqeq2d 2632	. . . . . . 7 |- ( w = B -> ( ( G NeighbVtx A ) = { A , w } <-> ( G NeighbVtx A ) = { A , B } ) )
30		preq2 4269	. . . . . . . 8 |- ( w = C -> { A , w } = { A , C } )
31	30	eqeq2d 2632	. . . . . . 7 |- ( w = C -> ( ( G NeighbVtx A ) = { A , w } <-> ( G NeighbVtx A ) = { A , C } ) )
32	29, 31	rexprg 4235	. . . . . 6 |- ( ( 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 } ) ) )
33	32	3adant1 1079	. . . . 5 |- ( ( 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 } ) ) )
34		preq2 4269	. . . . . . . . 9 |- ( w = C -> { B , w } = { B , C } )
35	34	eqeq2d 2632	. . . . . . . 8 |- ( w = C -> ( ( G NeighbVtx A ) = { B , w } <-> ( G NeighbVtx A ) = { B , C } ) )
36		preq2 4269	. . . . . . . . 9 |- ( w = A -> { B , w } = { B , A } )
37	36	eqeq2d 2632	. . . . . . . 8 |- ( w = A -> ( ( G NeighbVtx A ) = { B , w } <-> ( G NeighbVtx A ) = { B , A } ) )
38	35, 37	rexprg 4235	. . . . . . 7 |- ( ( 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 } ) ) )
39	38	ancoms 469	. . . . . 6 |- ( ( 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 } ) ) )
40	39	3adant2 1080	. . . . 5 |- ( ( 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 } ) ) )
41		preq2 4269	. . . . . . . 8 |- ( w = A -> { C , w } = { C , A } )
42	41	eqeq2d 2632	. . . . . . 7 |- ( w = A -> ( ( G NeighbVtx A ) = { C , w } <-> ( G NeighbVtx A ) = { C , A } ) )
43		preq2 4269	. . . . . . . 8 |- ( w = B -> { C , w } = { C , B } )
44	43	eqeq2d 2632	. . . . . . 7 |- ( w = B -> ( ( G NeighbVtx A ) = { C , w } <-> ( G NeighbVtx A ) = { C , B } ) )
45	42, 44	rexprg 4235	. . . . . 6 |- ( ( 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 } ) ) )
46	45	3adant3 1081	. . . . 5 |- ( ( 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 } ) ) )
47	33, 40, 46	3orbi123d 1398	. . . 4 |- ( ( 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 } ) ) ) )
48	1, 47	syl 17	. . 3 |- ( 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 } ) ) ) )
49		nb3grpr.n	. . . 4 |- ( ph -> ( A =/= B /\ A =/= C /\ B =/= C ) )
50		tprot 4284	. . . . . . . . 9 |- { A , B , C } = { B , C , A }
51	50	a1i 11	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> { A , B , C } = { B , C , A } )
52	51	difeq1d 3727	. . . . . . 7 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { A } ) = ( { B , C , A } \ { A } ) )
53		necom 2847	. . . . . . . . 9 |- ( A =/= B <-> B =/= A )
54		necom 2847	. . . . . . . . 9 |- ( A =/= C <-> C =/= A )
55		diftpsn3 4332	. . . . . . . . 9 |- ( ( B =/= A /\ C =/= A ) -> ( { B , C , A } \ { A } ) = { B , C } )
56	53, 54, 55	syl2anb 496	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C ) -> ( { B , C , A } \ { A } ) = { B , C } )
57	56	3adant3 1081	. . . . . . 7 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { B , C , A } \ { A } ) = { B , C } )
58	52, 57	eqtrd 2656	. . . . . 6 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { A } ) = { B , C } )
59	58	rexeqdv 3145	. . . . 5 |- ( ( 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 } ) )
60		tprot 4284	. . . . . . . . . 10 |- { C , A , B } = { A , B , C }
61	60	eqcomi 2631	. . . . . . . . 9 |- { A , B , C } = { C , A , B }
62	61	a1i 11	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> { A , B , C } = { C , A , B } )
63	62	difeq1d 3727	. . . . . . 7 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { B } ) = ( { C , A , B } \ { B } ) )
64		necom 2847	. . . . . . . . . . . 12 |- ( B =/= C <-> C =/= B )
65	64	anbi1i 731	. . . . . . . . . . 11 |- ( ( B =/= C /\ A =/= B ) <-> ( C =/= B /\ A =/= B ) )
66	65	biimpi 206	. . . . . . . . . 10 |- ( ( B =/= C /\ A =/= B ) -> ( C =/= B /\ A =/= B ) )
67	66	ancoms 469	. . . . . . . . 9 |- ( ( A =/= B /\ B =/= C ) -> ( C =/= B /\ A =/= B ) )
68		diftpsn3 4332	. . . . . . . . 9 |- ( ( C =/= B /\ A =/= B ) -> ( { C , A , B } \ { B } ) = { C , A } )
69	67, 68	syl 17	. . . . . . . 8 |- ( ( A =/= B /\ B =/= C ) -> ( { C , A , B } \ { B } ) = { C , A } )
70	69	3adant2 1080	. . . . . . 7 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { C , A , B } \ { B } ) = { C , A } )
71	63, 70	eqtrd 2656	. . . . . 6 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { B } ) = { C , A } )
72	71	rexeqdv 3145	. . . . 5 |- ( ( 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 } ) )
73		diftpsn3 4332	. . . . . . 7 |- ( ( A =/= C /\ B =/= C ) -> ( { A , B , C } \ { C } ) = { A , B } )
74	73	3adant1 1079	. . . . . 6 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { C } ) = { A , B } )
75	74	rexeqdv 3145	. . . . 5 |- ( ( 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 } ) )
76	59, 72, 75	3orbi123d 1398	. . . 4 |- ( ( 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 } ) ) )
77	49, 76	syl 17	. . 3 |- ( 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 } ) ) )
78		prcom 4267	. . . . . . . 8 |- { C , B } = { B , C }
79	78	eqeq2i 2634	. . . . . . 7 |- ( ( G NeighbVtx A ) = { C , B } <-> ( G NeighbVtx A ) = { B , C } )
80	79	orbi2i 541	. . . . . 6 |- ( ( ( G NeighbVtx A ) = { B , C } \/ ( G NeighbVtx A ) = { C , B } ) <-> ( ( G NeighbVtx A ) = { B , C } \/ ( G NeighbVtx A ) = { B , C } ) )
81		oridm 536	. . . . . 6 |- ( ( ( G NeighbVtx A ) = { B , C } \/ ( G NeighbVtx A ) = { B , C } ) <-> ( G NeighbVtx A ) = { B , C } )
82	80, 81	bitr2i 265	. . . . 5 |- ( ( G NeighbVtx A ) = { B , C } <-> ( ( G NeighbVtx A ) = { B , C } \/ ( G NeighbVtx A ) = { C , B } ) )
83	82	a1i 11	. . . 4 |- ( ph -> ( ( G NeighbVtx A ) = { B , C } <-> ( ( G NeighbVtx A ) = { B , C } \/ ( G NeighbVtx A ) = { C , B } ) ) )
84		usgrnbnself2 26262	. . . . . . . 8 |- ( G e. USGraph -> A e/ ( G NeighbVtx A ) )
85		df-nel 2898	. . . . . . . . 9 |- ( A e/ ( G NeighbVtx A ) <-> -. A e. ( G NeighbVtx A ) )
86		prid2g 4296	. . . . . . . . . . . 12 |- ( A e. X -> A e. { B , A } )
87	86	3ad2ant1 1082	. . . . . . . . . . 11 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> A e. { B , A } )
88		eleq2 2690	. . . . . . . . . . 11 |- ( ( G NeighbVtx A ) = { B , A } -> ( A e. ( G NeighbVtx A ) <-> A e. { B , A } ) )
89	87, 88	syl5ibrcom 237	. . . . . . . . . 10 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( ( G NeighbVtx A ) = { B , A } -> A e. ( G NeighbVtx A ) ) )
90	89	con3rr3 151	. . . . . . . . 9 |- ( -. A e. ( G NeighbVtx A ) -> ( ( A e. X /\ B e. Y /\ C e. Z ) -> -. ( G NeighbVtx A ) = { B , A } ) )
91	85, 90	sylbi 207	. . . . . . . 8 |- ( A e/ ( G NeighbVtx A ) -> ( ( A e. X /\ B e. Y /\ C e. Z ) -> -. ( G NeighbVtx A ) = { B , A } ) )
92	84, 91	syl 17	. . . . . . 7 |- ( G e. USGraph -> ( ( A e. X /\ B e. Y /\ C e. Z ) -> -. ( G NeighbVtx A ) = { B , A } ) )
93	20, 1, 92	sylc 65	. . . . . 6 |- ( ph -> -. ( G NeighbVtx A ) = { B , A } )
94		biorf 420	. . . . . . 7 |- ( -. ( G NeighbVtx A ) = { B , A } -> ( ( G NeighbVtx A ) = { B , C } <-> ( ( G NeighbVtx A ) = { B , A } \/ ( G NeighbVtx A ) = { B , C } ) ) )
95		orcom 402	. . . . . . 7 |- ( ( ( G NeighbVtx A ) = { B , A } \/ ( G NeighbVtx A ) = { B , C } ) <-> ( ( G NeighbVtx A ) = { B , C } \/ ( G NeighbVtx A ) = { B , A } ) )
96	94, 95	syl6bb 276	. . . . . 6 |- ( -. ( G NeighbVtx A ) = { B , A } -> ( ( G NeighbVtx A ) = { B , C } <-> ( ( G NeighbVtx A ) = { B , C } \/ ( G NeighbVtx A ) = { B , A } ) ) )
97	93, 96	syl 17	. . . . 5 |- ( ph -> ( ( G NeighbVtx A ) = { B , C } <-> ( ( G NeighbVtx A ) = { B , C } \/ ( G NeighbVtx A ) = { B , A } ) ) )
98		prid2g 4296	. . . . . . . . . . . 12 |- ( A e. X -> A e. { C , A } )
99	98	3ad2ant1 1082	. . . . . . . . . . 11 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> A e. { C , A } )
100		eleq2 2690	. . . . . . . . . . 11 |- ( ( G NeighbVtx A ) = { C , A } -> ( A e. ( G NeighbVtx A ) <-> A e. { C , A } ) )
101	99, 100	syl5ibrcom 237	. . . . . . . . . 10 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( ( G NeighbVtx A ) = { C , A } -> A e. ( G NeighbVtx A ) ) )
102	101	con3rr3 151	. . . . . . . . 9 |- ( -. A e. ( G NeighbVtx A ) -> ( ( A e. X /\ B e. Y /\ C e. Z ) -> -. ( G NeighbVtx A ) = { C , A } ) )
103	85, 102	sylbi 207	. . . . . . . 8 |- ( A e/ ( G NeighbVtx A ) -> ( ( A e. X /\ B e. Y /\ C e. Z ) -> -. ( G NeighbVtx A ) = { C , A } ) )
104	84, 103	syl 17	. . . . . . 7 |- ( G e. USGraph -> ( ( A e. X /\ B e. Y /\ C e. Z ) -> -. ( G NeighbVtx A ) = { C , A } ) )
105	20, 1, 104	sylc 65	. . . . . 6 |- ( ph -> -. ( G NeighbVtx A ) = { C , A } )
106		biorf 420	. . . . . 6 |- ( -. ( G NeighbVtx A ) = { C , A } -> ( ( G NeighbVtx A ) = { C , B } <-> ( ( G NeighbVtx A ) = { C , A } \/ ( G NeighbVtx A ) = { C , B } ) ) )
107	105, 106	syl 17	. . . . 5 |- ( ph -> ( ( G NeighbVtx A ) = { C , B } <-> ( ( G NeighbVtx A ) = { C , A } \/ ( G NeighbVtx A ) = { C , B } ) ) )
108	97, 107	orbi12d 746	. . . 4 |- ( 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 4295	. . . . . . . . . . . . . 14 |- ( A e. X -> A e. { A , B } )
110	109	3ad2ant1 1082	. . . . . . . . . . . . 13 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> A e. { A , B } )
111		eleq2 2690	. . . . . . . . . . . . 13 |- ( ( G NeighbVtx A ) = { A , B } -> ( A e. ( G NeighbVtx A ) <-> A e. { A , B } ) )
112	110, 111	syl5ibrcom 237	. . . . . . . . . . . 12 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( ( G NeighbVtx A ) = { A , B } -> A e. ( G NeighbVtx A ) ) )
113	112	con3dimp 457	. . . . . . . . . . 11 |- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ -. A e. ( G NeighbVtx A ) ) -> -. ( G NeighbVtx A ) = { A , B } )
114		prid1g 4295	. . . . . . . . . . . . . 14 |- ( A e. X -> A e. { A , C } )
115	114	3ad2ant1 1082	. . . . . . . . . . . . 13 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> A e. { A , C } )
116		eleq2 2690	. . . . . . . . . . . . 13 |- ( ( G NeighbVtx A ) = { A , C } -> ( A e. ( G NeighbVtx A ) <-> A e. { A , C } ) )
117	115, 116	syl5ibrcom 237	. . . . . . . . . . . 12 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( ( G NeighbVtx A ) = { A , C } -> A e. ( G NeighbVtx A ) ) )
118	117	con3dimp 457	. . . . . . . . . . 11 |- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ -. A e. ( G NeighbVtx A ) ) -> -. ( G NeighbVtx A ) = { A , C } )
119	113, 118	jca 554	. . . . . . . . . 10 |- ( ( ( 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 451	. . . . . . . . 9 |- ( -. 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	85, 120	sylbi 207	. . . . . . . 8 |- ( 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	84, 121	syl 17	. . . . . . 7 |- ( G e. USGraph -> ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( -. ( G NeighbVtx A ) = { A , B } /\ -. ( G NeighbVtx A ) = { A , C } ) ) )
123	20, 1, 122	sylc 65	. . . . . 6 |- ( ph -> ( -. ( G NeighbVtx A ) = { A , B } /\ -. ( G NeighbVtx A ) = { A , C } ) )
124		ioran 511	. . . . . 6 |- ( -. ( ( G NeighbVtx A ) = { A , B } \/ ( G NeighbVtx A ) = { A , C } ) <-> ( -. ( G NeighbVtx A ) = { A , B } /\ -. ( G NeighbVtx A ) = { A , C } ) )
125	123, 124	sylibr 224	. . . . 5 |- ( ph -> -. ( ( G NeighbVtx A ) = { A , B } \/ ( G NeighbVtx A ) = { A , C } ) )
126	125	3bior1fd 1438	. . . 4 |- ( 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 } ) ) ) )
127	83, 108, 126	3bitrd 294	. . 3 |- ( 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 } ) ) ) )
128	48, 77, 127	3bitr4rd 301	. 2 |- ( 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 } ) ) )
129	18, 27, 128	3bitr4rd 301	1 |- ( ph -> ( ( G NeighbVtx A ) = { B , C } <-> E. v e. V E. w e. ( V \ { v } ) ( G NeighbVtx A ) = { v , w } ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   \/ w3o 1036   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   e/ wnel 2897   E.wrex 2913   \ cdif 3571   {csn 4177   {cpr 4179   {ctp 4181   ` cfv 5888  (class class class)co 6650  Vtxcvtx 25874  Edgcedg 25939   USGraph cusgr 26044   NeighbVtx cnbgr 26224

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-1st 7168  df-2nd 7169  df-nbgr 26228

This theorem is referenced by:  nb3grpr  26284