Theorem nb3grprlem2 29308

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

Hypotheses

Ref	Expression
nb3grpr.v	⊢ 𝑉 = (Vtx‘𝐺)
nb3grpr.e	⊢ 𝐸 = (Edg‘𝐺)
nb3grpr.g	⊢ (𝜑 → 𝐺 ∈ USGraph)
nb3grpr.t	⊢ (𝜑 → 𝑉 = {𝐴, 𝐵, 𝐶})
nb3grpr.s	⊢ (𝜑 → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍))
nb3grpr.n	⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))

Assertion

Ref	Expression
nb3grprlem2	⊢ (𝜑 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ∃𝑣 ∈ 𝑉 ∃𝑤 ∈ (𝑉 ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤}))

Distinct variable groups:   𝑣,𝐴   𝑣,𝐵   𝑣,𝐶   𝑣,𝐸   𝑣,𝐺   𝑣,𝑉   𝜑,𝑣   𝑤,𝐴,𝑣   𝑤,𝐵   𝑤,𝐶   𝑤,𝐺   𝑤,𝑉

Allowed substitution hints:   𝜑(𝑤)   𝐸(𝑤)   𝑋(𝑤,𝑣)   𝑌(𝑤,𝑣)   𝑍(𝑤,𝑣)

Proof of Theorem nb3grprlem2

Step	Hyp	Ref	Expression
1		nb3grpr.s	. . 3 ⊢ (𝜑 → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍))
2		sneq 4599	. . . . . 6 ⊢ (𝑣 = 𝐴 → {𝑣} = {𝐴})
3	2	difeq2d 4089	. . . . 5 ⊢ (𝑣 = 𝐴 → ({𝐴, 𝐵, 𝐶} ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐴}))
4		preq1 4697	. . . . . 6 ⊢ (𝑣 = 𝐴 → {𝑣, 𝑤} = {𝐴, 𝑤})
5	4	eqeq2d 2740	. . . . 5 ⊢ (𝑣 = 𝐴 → ((𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤}))
6	3, 5	rexeqbidv 3320	. . . 4 ⊢ (𝑣 = 𝐴 → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤}))
7		sneq 4599	. . . . . 6 ⊢ (𝑣 = 𝐵 → {𝑣} = {𝐵})
8	7	difeq2d 4089	. . . . 5 ⊢ (𝑣 = 𝐵 → ({𝐴, 𝐵, 𝐶} ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐵}))
9		preq1 4697	. . . . . 6 ⊢ (𝑣 = 𝐵 → {𝑣, 𝑤} = {𝐵, 𝑤})
10	9	eqeq2d 2740	. . . . 5 ⊢ (𝑣 = 𝐵 → ((𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤}))
11	8, 10	rexeqbidv 3320	. . . 4 ⊢ (𝑣 = 𝐵 → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤}))
12		sneq 4599	. . . . . 6 ⊢ (𝑣 = 𝐶 → {𝑣} = {𝐶})
13	12	difeq2d 4089	. . . . 5 ⊢ (𝑣 = 𝐶 → ({𝐴, 𝐵, 𝐶} ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐶}))
14		preq1 4697	. . . . . 6 ⊢ (𝑣 = 𝐶 → {𝑣, 𝑤} = {𝐶, 𝑤})
15	14	eqeq2d 2740	. . . . 5 ⊢ (𝑣 = 𝐶 → ((𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤}))
16	13, 15	rexeqbidv 3320	. . . 4 ⊢ (𝑣 = 𝐶 → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤}))
17	6, 11, 16	rextpg 4663	. . 3 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∃𝑣 ∈ {𝐴, 𝐵, 𝐶}∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤})))
18	1, 17	syl 17	. 2 ⊢ (𝜑 → (∃𝑣 ∈ {𝐴, 𝐵, 𝐶}∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤})))
19		nb3grpr.t	. . . 4 ⊢ (𝜑 → 𝑉 = {𝐴, 𝐵, 𝐶})
20		nb3grpr.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ USGraph)
21	19, 20	jca 511	. . 3 ⊢ (𝜑 → (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph))
22		simpl 482	. . . 4 ⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → 𝑉 = {𝐴, 𝐵, 𝐶})
23		difeq1 4082	. . . . . 6 ⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → (𝑉 ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝑣}))
24	23	adantr 480	. . . . 5 ⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝑉 ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝑣}))
25	24	rexeqdv 3300	. . . 4 ⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (∃𝑤 ∈ (𝑉 ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤}))
26	22, 25	rexeqbidv 3320	. . 3 ⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (∃𝑣 ∈ 𝑉 ∃𝑤 ∈ (𝑉 ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ ∃𝑣 ∈ {𝐴, 𝐵, 𝐶}∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤}))
27	21, 26	syl 17	. 2 ⊢ (𝜑 → (∃𝑣 ∈ 𝑉 ∃𝑤 ∈ (𝑉 ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ ∃𝑣 ∈ {𝐴, 𝐵, 𝐶}∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤}))
28		preq2 4698	. . . . . . . 8 ⊢ (𝑤 = 𝐵 → {𝐴, 𝑤} = {𝐴, 𝐵})
29	28	eqeq2d 2740	. . . . . . 7 ⊢ (𝑤 = 𝐵 → ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵}))
30		preq2 4698	. . . . . . . 8 ⊢ (𝑤 = 𝐶 → {𝐴, 𝑤} = {𝐴, 𝐶})
31	30	eqeq2d 2740	. . . . . . 7 ⊢ (𝑤 = 𝐶 → ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}))
32	29, 31	rexprg 4661	. . . . . 6 ⊢ ((𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∃𝑤 ∈ {𝐵, 𝐶} (𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∨ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶})))
33	32	3adant1 1130	. . . . 5 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∃𝑤 ∈ {𝐵, 𝐶} (𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∨ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶})))
34		preq2 4698	. . . . . . . . 9 ⊢ (𝑤 = 𝐶 → {𝐵, 𝑤} = {𝐵, 𝐶})
35	34	eqeq2d 2740	. . . . . . . 8 ⊢ (𝑤 = 𝐶 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶}))
36		preq2 4698	. . . . . . . . 9 ⊢ (𝑤 = 𝐴 → {𝐵, 𝑤} = {𝐵, 𝐴})
37	36	eqeq2d 2740	. . . . . . . 8 ⊢ (𝑤 = 𝐴 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴}))
38	35, 37	rexprg 4661	. . . . . . 7 ⊢ ((𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋) → (∃𝑤 ∈ {𝐶, 𝐴} (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴})))
39	38	ancoms 458	. . . . . 6 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍) → (∃𝑤 ∈ {𝐶, 𝐴} (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴})))
40	39	3adant2 1131	. . . . 5 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∃𝑤 ∈ {𝐶, 𝐴} (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴})))
41		preq2 4698	. . . . . . . 8 ⊢ (𝑤 = 𝐴 → {𝐶, 𝑤} = {𝐶, 𝐴})
42	41	eqeq2d 2740	. . . . . . 7 ⊢ (𝑤 = 𝐴 → ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴}))
43		preq2 4698	. . . . . . . 8 ⊢ (𝑤 = 𝐵 → {𝐶, 𝑤} = {𝐶, 𝐵})
44	43	eqeq2d 2740	. . . . . . 7 ⊢ (𝑤 = 𝐵 → ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵}))
45	42, 44	rexprg 4661	. . . . . 6 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → (∃𝑤 ∈ {𝐴, 𝐵} (𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵})))
46	45	3adant3 1132	. . . . 5 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∃𝑤 ∈ {𝐴, 𝐵} (𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵})))
47	33, 40, 46	3orbi123d 1437	. . . 4 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((∃𝑤 ∈ {𝐵, 𝐶} (𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ {𝐶, 𝐴} (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ {𝐴, 𝐵} (𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤}) ↔ (((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∨ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}) ∨ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴}) ∨ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵}))))
48	1, 47	syl 17	. . 3 ⊢ (𝜑 → ((∃𝑤 ∈ {𝐵, 𝐶} (𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ {𝐶, 𝐴} (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ {𝐴, 𝐵} (𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤}) ↔ (((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∨ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}) ∨ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴}) ∨ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵}))))
49		nb3grpr.n	. . . 4 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))
50		tprot 4713	. . . . . . . . 9 ⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴}
51	50	a1i 11	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴})
52	51	difeq1d 4088	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐴}) = ({𝐵, 𝐶, 𝐴} ∖ {𝐴}))
53		necom 2978	. . . . . . . . 9 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)
54		necom 2978	. . . . . . . . 9 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐶 ≠ 𝐴)
55		diftpsn3 4766	. . . . . . . . 9 ⊢ ((𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶})
56	53, 54, 55	syl2anb 598	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶})
57	56	3adant3 1132	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶})
58	52, 57	eqtrd 2764	. . . . . 6 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐴}) = {𝐵, 𝐶})
59	58	rexeqdv 3300	. . . . 5 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ↔ ∃𝑤 ∈ {𝐵, 𝐶} (𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤}))
60		tprot 4713	. . . . . . . . . 10 ⊢ {𝐶, 𝐴, 𝐵} = {𝐴, 𝐵, 𝐶}
61	60	eqcomi 2738	. . . . . . . . 9 ⊢ {𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵}
62	61	a1i 11	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → {𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵})
63	62	difeq1d 4088	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐵}) = ({𝐶, 𝐴, 𝐵} ∖ {𝐵}))
64		necom 2978	. . . . . . . . . . . 12 ⊢ (𝐵 ≠ 𝐶 ↔ 𝐶 ≠ 𝐵)
65	64	anbi1i 624	. . . . . . . . . . 11 ⊢ ((𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵) ↔ (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵))
66	65	biimpi 216	. . . . . . . . . 10 ⊢ ((𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵) → (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵))
67	66	ancoms 458	. . . . . . . . 9 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) → (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵))
68		diftpsn3 4766	. . . . . . . . 9 ⊢ ((𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴})
69	67, 68	syl 17	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴})
70	69	3adant2 1131	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴})
71	63, 70	eqtrd 2764	. . . . . 6 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐵}) = {𝐶, 𝐴})
72	71	rexeqdv 3300	. . . . 5 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ↔ ∃𝑤 ∈ {𝐶, 𝐴} (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤}))
73		diftpsn3 4766	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
74	73	3adant1 1130	. . . . . 6 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
75	74	rexeqdv 3300	. . . . 5 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤} ↔ ∃𝑤 ∈ {𝐴, 𝐵} (𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤}))
76	59, 72, 75	3orbi123d 1437	. . . 4 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ((∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤}) ↔ (∃𝑤 ∈ {𝐵, 𝐶} (𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ {𝐶, 𝐴} (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ {𝐴, 𝐵} (𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤})))
77	49, 76	syl 17	. . 3 ⊢ (𝜑 → ((∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤}) ↔ (∃𝑤 ∈ {𝐵, 𝐶} (𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ {𝐶, 𝐴} (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ {𝐴, 𝐵} (𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤})))
78		prcom 4696	. . . . . . . 8 ⊢ {𝐶, 𝐵} = {𝐵, 𝐶}
79	78	eqeq2i 2742	. . . . . . 7 ⊢ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵} ↔ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶})
80	79	orbi2i 912	. . . . . 6 ⊢ (((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵}) ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶}))
81		oridm 904	. . . . . 6 ⊢ (((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶}) ↔ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶})
82	80, 81	bitr2i 276	. . . . 5 ⊢ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵}))
83	82	a1i 11	. . . 4 ⊢ (𝜑 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵})))
84		nbgrnself2 29287	. . . . . . 7 ⊢ 𝐴 ∉ (𝐺 NeighbVtx 𝐴)
85		df-nel 3030	. . . . . . . 8 ⊢ (𝐴 ∉ (𝐺 NeighbVtx 𝐴) ↔ ¬ 𝐴 ∈ (𝐺 NeighbVtx 𝐴))
86		prid2g 4725	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝑋 → 𝐴 ∈ {𝐵, 𝐴})
87	86	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → 𝐴 ∈ {𝐵, 𝐴})
88		eleq2 2817	. . . . . . . . . 10 ⊢ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴} → (𝐴 ∈ (𝐺 NeighbVtx 𝐴) ↔ 𝐴 ∈ {𝐵, 𝐴}))
89	87, 88	syl5ibrcom 247	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴} → 𝐴 ∈ (𝐺 NeighbVtx 𝐴)))
90	89	con3rr3 155	. . . . . . . 8 ⊢ (¬ 𝐴 ∈ (𝐺 NeighbVtx 𝐴) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ¬ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴}))
91	85, 90	sylbi 217	. . . . . . 7 ⊢ (𝐴 ∉ (𝐺 NeighbVtx 𝐴) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ¬ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴}))
92	84, 1, 91	mpsyl 68	. . . . . 6 ⊢ (𝜑 → ¬ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴})
93		biorf 936	. . . . . . 7 ⊢ (¬ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴} → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶})))
94		orcom 870	. . . . . . 7 ⊢ (((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶}) ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴}))
95	93, 94	bitrdi 287	. . . . . 6 ⊢ (¬ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴} → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴})))
96	92, 95	syl 17	. . . . 5 ⊢ (𝜑 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴})))
97		prid2g 4725	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝑋 → 𝐴 ∈ {𝐶, 𝐴})
98	97	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → 𝐴 ∈ {𝐶, 𝐴})
99		eleq2 2817	. . . . . . . . . 10 ⊢ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} → (𝐴 ∈ (𝐺 NeighbVtx 𝐴) ↔ 𝐴 ∈ {𝐶, 𝐴}))
100	98, 99	syl5ibrcom 247	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} → 𝐴 ∈ (𝐺 NeighbVtx 𝐴)))
101	100	con3rr3 155	. . . . . . . 8 ⊢ (¬ 𝐴 ∈ (𝐺 NeighbVtx 𝐴) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ¬ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴}))
102	85, 101	sylbi 217	. . . . . . 7 ⊢ (𝐴 ∉ (𝐺 NeighbVtx 𝐴) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ¬ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴}))
103	84, 1, 102	mpsyl 68	. . . . . 6 ⊢ (𝜑 → ¬ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴})
104		biorf 936	. . . . . 6 ⊢ (¬ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} → ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵})))
105	103, 104	syl 17	. . . . 5 ⊢ (𝜑 → ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵})))
106	96, 105	orbi12d 918	. . . 4 ⊢ (𝜑 → (((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵}) ↔ (((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴}) ∨ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵}))))
107		prid1g 4724	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ 𝑋 → 𝐴 ∈ {𝐴, 𝐵})
108	107	3ad2ant1 1133	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → 𝐴 ∈ {𝐴, 𝐵})
109		eleq2 2817	. . . . . . . . . . . 12 ⊢ ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} → (𝐴 ∈ (𝐺 NeighbVtx 𝐴) ↔ 𝐴 ∈ {𝐴, 𝐵}))
110	108, 109	syl5ibrcom 247	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} → 𝐴 ∈ (𝐺 NeighbVtx 𝐴)))
111	110	con3dimp 408	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ ¬ 𝐴 ∈ (𝐺 NeighbVtx 𝐴)) → ¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵})
112		prid1g 4724	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ 𝑋 → 𝐴 ∈ {𝐴, 𝐶})
113	112	3ad2ant1 1133	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → 𝐴 ∈ {𝐴, 𝐶})
114		eleq2 2817	. . . . . . . . . . . 12 ⊢ ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶} → (𝐴 ∈ (𝐺 NeighbVtx 𝐴) ↔ 𝐴 ∈ {𝐴, 𝐶}))
115	113, 114	syl5ibrcom 247	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶} → 𝐴 ∈ (𝐺 NeighbVtx 𝐴)))
116	115	con3dimp 408	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ ¬ 𝐴 ∈ (𝐺 NeighbVtx 𝐴)) → ¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶})
117	111, 116	jca 511	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ ¬ 𝐴 ∈ (𝐺 NeighbVtx 𝐴)) → (¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∧ ¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}))
118	117	expcom 413	. . . . . . . 8 ⊢ (¬ 𝐴 ∈ (𝐺 NeighbVtx 𝐴) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∧ ¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶})))
119	85, 118	sylbi 217	. . . . . . 7 ⊢ (𝐴 ∉ (𝐺 NeighbVtx 𝐴) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∧ ¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶})))
120	84, 1, 119	mpsyl 68	. . . . . 6 ⊢ (𝜑 → (¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∧ ¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}))
121		ioran 985	. . . . . 6 ⊢ (¬ ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∨ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}) ↔ (¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∧ ¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}))
122	120, 121	sylibr 234	. . . . 5 ⊢ (𝜑 → ¬ ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∨ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}))
123	122	3bior1fd 1477	. . . 4 ⊢ (𝜑 → ((((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴}) ∨ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵})) ↔ (((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∨ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}) ∨ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴}) ∨ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵}))))
124	83, 106, 123	3bitrd 305	. . 3 ⊢ (𝜑 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ (((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∨ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}) ∨ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴}) ∨ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵}))))
125	48, 77, 124	3bitr4rd 312	. 2 ⊢ (𝜑 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤})))
126	18, 27, 125	3bitr4rd 312	1 ⊢ (𝜑 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ∃𝑣 ∈ 𝑉 ∃𝑤 ∈ (𝑉 ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤}))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∨ w3o 1085   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2925   ∉ wnel 3029  ∃wrex 3053   ∖ cdif 3911  {csn 4589  {cpr 4591  {ctp 4593  ‘cfv 6511  (class class class)co 7387  Vtxcvtx 28923  Edgcedg 28974  USGraphcusgr 29076   NeighbVtx cnbgr 29259

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-tp 4594  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fv 6519  df-ov 7390  df-oprab 7391  df-mpo 7392  df-1st 7968  df-2nd 7969  df-nbgr 29260

This theorem is referenced by:  nb3grpr  29309