Theorem nb3grprlem2 39619

Description: Lemma 2 for nb3grapr 25260. (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 3969	. . . . . 6 |- ( v = A -> { v } = { A } )
3	2	difeq2d 3540	. . . . 5 |- ( v = A -> ( { A , B , C } \ { v } ) = ( { A , B , C } \ { A } ) )
4		preq1 4042	. . . . . 6 |- ( v = A -> { v , w } = { A , w } )
5	4	eqeq2d 2481	. . . . 5 |- ( v = A -> ( ( G NeighbVtx A ) = { v , w } <-> ( G NeighbVtx A ) = { A , w } ) )
6	3, 5	rexeqbidv 2988	. . . 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 3969	. . . . . 6 |- ( v = B -> { v } = { B } )
8	7	difeq2d 3540	. . . . 5 |- ( v = B -> ( { A , B , C } \ { v } ) = ( { A , B , C } \ { B } ) )
9		preq1 4042	. . . . . 6 |- ( v = B -> { v , w } = { B , w } )
10	9	eqeq2d 2481	. . . . 5 |- ( v = B -> ( ( G NeighbVtx A ) = { v , w } <-> ( G NeighbVtx A ) = { B , w } ) )
11	8, 10	rexeqbidv 2988	. . . 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 3969	. . . . . 6 |- ( v = C -> { v } = { C } )
13	12	difeq2d 3540	. . . . 5 |- ( v = C -> ( { A , B , C } \ { v } ) = ( { A , B , C } \ { C } ) )
14		preq1 4042	. . . . . 6 |- ( v = C -> { v , w } = { C , w } )
15	14	eqeq2d 2481	. . . . 5 |- ( v = C -> ( ( G NeighbVtx A ) = { v , w } <-> ( G NeighbVtx A ) = { C , w } ) )
16	13, 15	rexeqbidv 2988	. . . 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 4015	. . 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 541	. . 3 |- ( ph -> ( V = { A , B , C } /\ G e. USGraph ) )
22		simpl 464	. . . 4 |- ( ( V = { A , B , C } /\ G e. USGraph ) -> V = { A , B , C } )
23		difeq1 3533	. . . . . 6 |- ( V = { A , B , C } -> ( V \ { v } ) = ( { A , B , C } \ { v } ) )
24	23	adantr 472	. . . . 5 |- ( ( V = { A , B , C } /\ G e. USGraph ) -> ( V \ { v } ) = ( { A , B , C } \ { v } ) )
25	24	rexeqdv 2980	. . . 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 2988	. . 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 4043	. . . . . . . 8 |- ( w = B -> { A , w } = { A , B } )
29	28	eqeq2d 2481	. . . . . . 7 |- ( w = B -> ( ( G NeighbVtx A ) = { A , w } <-> ( G NeighbVtx A ) = { A , B } ) )
30		preq2 4043	. . . . . . . 8 |- ( w = C -> { A , w } = { A , C } )
31	30	eqeq2d 2481	. . . . . . 7 |- ( w = C -> ( ( G NeighbVtx A ) = { A , w } <-> ( G NeighbVtx A ) = { A , C } ) )
32	29, 31	rexprg 4013	. . . . . 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 1048	. . . . 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 4043	. . . . . . . . 9 |- ( w = C -> { B , w } = { B , C } )
35	34	eqeq2d 2481	. . . . . . . 8 |- ( w = C -> ( ( G NeighbVtx A ) = { B , w } <-> ( G NeighbVtx A ) = { B , C } ) )
36		preq2 4043	. . . . . . . . 9 |- ( w = A -> { B , w } = { B , A } )
37	36	eqeq2d 2481	. . . . . . . 8 |- ( w = A -> ( ( G NeighbVtx A ) = { B , w } <-> ( G NeighbVtx A ) = { B , A } ) )
38	35, 37	rexprg 4013	. . . . . . 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 460	. . . . . 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 1049	. . . . 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 4043	. . . . . . . 8 |- ( w = A -> { C , w } = { C , A } )
42	41	eqeq2d 2481	. . . . . . 7 |- ( w = A -> ( ( G NeighbVtx A ) = { C , w } <-> ( G NeighbVtx A ) = { C , A } ) )
43		preq2 4043	. . . . . . . 8 |- ( w = B -> { C , w } = { C , B } )
44	43	eqeq2d 2481	. . . . . . 7 |- ( w = B -> ( ( G NeighbVtx A ) = { C , w } <-> ( G NeighbVtx A ) = { C , B } ) )
45	42, 44	rexprg 4013	. . . . . 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 1050	. . . . 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 1364	. . . 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 4058	. . . . . . . . 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 3539	. . . . . . 7 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { A } ) = ( { B , C , A } \ { A } ) )
53		necom 2696	. . . . . . . . 9 |- ( A =/= B <-> B =/= A )
54		necom 2696	. . . . . . . . 9 |- ( A =/= C <-> C =/= A )
55		diftpsn3 4101	. . . . . . . . 9 |- ( ( B =/= A /\ C =/= A ) -> ( { B , C , A } \ { A } ) = { B , C } )
56	53, 54, 55	syl2anb 487	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C ) -> ( { B , C , A } \ { A } ) = { B , C } )
57	56	3adant3 1050	. . . . . . 7 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { B , C , A } \ { A } ) = { B , C } )
58	52, 57	eqtrd 2505	. . . . . 6 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { A } ) = { B , C } )
59	58	rexeqdv 2980	. . . . 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 4058	. . . . . . . . . 10 |- { C , A , B } = { A , B , C }
61	60	eqcomi 2480	. . . . . . . . 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 3539	. . . . . . 7 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { B } ) = ( { C , A , B } \ { B } ) )
64		necom 2696	. . . . . . . . . . . 12 |- ( B =/= C <-> C =/= B )
65	64	anbi1i 709	. . . . . . . . . . 11 |- ( ( B =/= C /\ A =/= B ) <-> ( C =/= B /\ A =/= B ) )
66	65	biimpi 199	. . . . . . . . . 10 |- ( ( B =/= C /\ A =/= B ) -> ( C =/= B /\ A =/= B ) )
67	66	ancoms 460	. . . . . . . . 9 |- ( ( A =/= B /\ B =/= C ) -> ( C =/= B /\ A =/= B ) )
68		diftpsn3 4101	. . . . . . . . 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 1049	. . . . . . 7 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { C , A , B } \ { B } ) = { C , A } )
71	63, 70	eqtrd 2505	. . . . . 6 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { B } ) = { C , A } )
72	71	rexeqdv 2980	. . . . 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 4101	. . . . . . 7 |- ( ( A =/= C /\ B =/= C ) -> ( { A , B , C } \ { C } ) = { A , B } )
74	73	3adant1 1048	. . . . . 6 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { C } ) = { A , B } )
75	74	rexeqdv 2980	. . . . 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 1364	. . . 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 4041	. . . . . . . 8 |- { C , B } = { B , C }
79	78	eqeq2i 2483	. . . . . . 7 |- ( ( G NeighbVtx A ) = { C , B } <-> ( G NeighbVtx A ) = { B , C } )
80	79	orbi2i 528	. . . . . 6 |- ( ( ( G NeighbVtx A ) = { B , C } \/ ( G NeighbVtx A ) = { C , B } ) <-> ( ( G NeighbVtx A ) = { B , C } \/ ( G NeighbVtx A ) = { B , C } ) )
81		oridm 523	. . . . . 6 |- ( ( ( G NeighbVtx A ) = { B , C } \/ ( G NeighbVtx A ) = { B , C } ) <-> ( G NeighbVtx A ) = { B , C } )
82	80, 81	bitr2i 258	. . . . 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 39598	. . . . . . . 8 |- ( G e. USGraph -> A e/ ( G NeighbVtx A ) )
85		df-nel 2644	. . . . . . . . 9 |- ( A e/ ( G NeighbVtx A ) <-> -. A e. ( G NeighbVtx A ) )
86		prid2g 4070	. . . . . . . . . . . 12 |- ( A e. X -> A e. { B , A } )
87	86	3ad2ant1 1051	. . . . . . . . . . 11 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> A e. { B , A } )
88		eleq2 2538	. . . . . . . . . . 11 |- ( ( G NeighbVtx A ) = { B , A } -> ( A e. ( G NeighbVtx A ) <-> A e. { B , A } ) )
89	87, 88	syl5ibrcom 230	. . . . . . . . . 10 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( ( G NeighbVtx A ) = { B , A } -> A e. ( G NeighbVtx A ) ) )
90	89	con3rr3 143	. . . . . . . . 9 |- ( -. A e. ( G NeighbVtx A ) -> ( ( A e. X /\ B e. Y /\ C e. Z ) -> -. ( G NeighbVtx A ) = { B , A } ) )
91	85, 90	sylbi 200	. . . . . . . 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 61	. . . . . 6 |- ( ph -> -. ( G NeighbVtx A ) = { B , A } )
94		biorf 412	. . . . . . 7 |- ( -. ( G NeighbVtx A ) = { B , A } -> ( ( G NeighbVtx A ) = { B , C } <-> ( ( G NeighbVtx A ) = { B , A } \/ ( G NeighbVtx A ) = { B , C } ) ) )
95		orcom 394	. . . . . . 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 269	. . . . . 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 4070	. . . . . . . . . . . 12 |- ( A e. X -> A e. { C , A } )
99	98	3ad2ant1 1051	. . . . . . . . . . 11 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> A e. { C , A } )
100		eleq2 2538	. . . . . . . . . . 11 |- ( ( G NeighbVtx A ) = { C , A } -> ( A e. ( G NeighbVtx A ) <-> A e. { C , A } ) )
101	99, 100	syl5ibrcom 230	. . . . . . . . . 10 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( ( G NeighbVtx A ) = { C , A } -> A e. ( G NeighbVtx A ) ) )
102	101	con3rr3 143	. . . . . . . . 9 |- ( -. A e. ( G NeighbVtx A ) -> ( ( A e. X /\ B e. Y /\ C e. Z ) -> -. ( G NeighbVtx A ) = { C , A } ) )
103	85, 102	sylbi 200	. . . . . . . 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 61	. . . . . 6 |- ( ph -> -. ( G NeighbVtx A ) = { C , A } )
106		biorf 412	. . . . . 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 724	. . . 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 4069	. . . . . . . . . . . . . 14 |- ( A e. X -> A e. { A , B } )
110	109	3ad2ant1 1051	. . . . . . . . . . . . 13 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> A e. { A , B } )
111		eleq2 2538	. . . . . . . . . . . . 13 |- ( ( G NeighbVtx A ) = { A , B } -> ( A e. ( G NeighbVtx A ) <-> A e. { A , B } ) )
112	110, 111	syl5ibrcom 230	. . . . . . . . . . . 12 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( ( G NeighbVtx A ) = { A , B } -> A e. ( G NeighbVtx A ) ) )
113	112	con3dimp 448	. . . . . . . . . . 11 |- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ -. A e. ( G NeighbVtx A ) ) -> -. ( G NeighbVtx A ) = { A , B } )
114		prid1g 4069	. . . . . . . . . . . . . 14 |- ( A e. X -> A e. { A , C } )
115	114	3ad2ant1 1051	. . . . . . . . . . . . 13 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> A e. { A , C } )
116		eleq2 2538	. . . . . . . . . . . . 13 |- ( ( G NeighbVtx A ) = { A , C } -> ( A e. ( G NeighbVtx A ) <-> A e. { A , C } ) )
117	115, 116	syl5ibrcom 230	. . . . . . . . . . . 12 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( ( G NeighbVtx A ) = { A , C } -> A e. ( G NeighbVtx A ) ) )
118	117	con3dimp 448	. . . . . . . . . . 11 |- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ -. A e. ( G NeighbVtx A ) ) -> -. ( G NeighbVtx A ) = { A , C } )
119	113, 118	jca 541	. . . . . . . . . 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 442	. . . . . . . . 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 200	. . . . . . . 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 61	. . . . . 6 |- ( ph -> ( -. ( G NeighbVtx A ) = { A , B } /\ -. ( G NeighbVtx A ) = { A , C } ) )
124		ioran 498	. . . . . 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 217	. . . . 5 |- ( ph -> -. ( ( G NeighbVtx A ) = { A , B } \/ ( G NeighbVtx A ) = { A , C } ) )
126	125	3bior1fd 1403	. . . 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 287	. . 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 294	. 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 294	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 189   \/ wo 375   /\ wa 376   \/ w3o 1006   /\ w3a 1007   = wceq 1452   e. wcel 1904   =/= wne 2641   e/ wnel 2642   E.wrex 2757   \ cdif 3387   {csn 3959   {cpr 3961   {ctp 3963   ` cfv 5589  (class class class)co 6308  Vtxcvtx 39251  Edgcedga 39371   USGraph cusgr 39397   NeighbVtx cnbgr 39561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-fal 1458  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-iota 5553  df-fun 5591  df-fv 5597  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-1st 6812  df-2nd 6813  df-nbgr 39565

This theorem is referenced by:  nb3grpr  39620