Theorem nb3grprlem2 27748

Description: Lemma 2 for nb3grpr 27749. (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 4571	. . . . . 6 ⊢ (𝑣 = 𝐴 → {𝑣} = {𝐴})
3	2	difeq2d 4057	. . . . 5 ⊢ (𝑣 = 𝐴 → ({𝐴, 𝐵, 𝐶} ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐴}))
4		preq1 4669	. . . . . 6 ⊢ (𝑣 = 𝐴 → {𝑣, 𝑤} = {𝐴, 𝑤})
5	4	eqeq2d 2749	. . . . 5 ⊢ (𝑣 = 𝐴 → ((𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤}))
6	3, 5	rexeqbidv 3337	. . . 4 ⊢ (𝑣 = 𝐴 → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤}))
7		sneq 4571	. . . . . 6 ⊢ (𝑣 = 𝐵 → {𝑣} = {𝐵})
8	7	difeq2d 4057	. . . . 5 ⊢ (𝑣 = 𝐵 → ({𝐴, 𝐵, 𝐶} ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐵}))
9		preq1 4669	. . . . . 6 ⊢ (𝑣 = 𝐵 → {𝑣, 𝑤} = {𝐵, 𝑤})
10	9	eqeq2d 2749	. . . . 5 ⊢ (𝑣 = 𝐵 → ((𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤}))
11	8, 10	rexeqbidv 3337	. . . 4 ⊢ (𝑣 = 𝐵 → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤}))
12		sneq 4571	. . . . . 6 ⊢ (𝑣 = 𝐶 → {𝑣} = {𝐶})
13	12	difeq2d 4057	. . . . 5 ⊢ (𝑣 = 𝐶 → ({𝐴, 𝐵, 𝐶} ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐶}))
14		preq1 4669	. . . . . 6 ⊢ (𝑣 = 𝐶 → {𝑣, 𝑤} = {𝐶, 𝑤})
15	14	eqeq2d 2749	. . . . 5 ⊢ (𝑣 = 𝐶 → ((𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤}))
16	13, 15	rexeqbidv 3337	. . . 4 ⊢ (𝑣 = 𝐶 → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤}))
17	6, 11, 16	rextpg 4635	. . 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 512	. . 3 ⊢ (𝜑 → (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph))
22		simpl 483	. . . 4 ⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → 𝑉 = {𝐴, 𝐵, 𝐶})
23		difeq1 4050	. . . . . 6 ⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → (𝑉 ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝑣}))
24	23	adantr 481	. . . . 5 ⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝑉 ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝑣}))
25	24	rexeqdv 3349	. . . 4 ⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (∃𝑤 ∈ (𝑉 ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤}))
26	22, 25	rexeqbidv 3337	. . 3 ⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (∃𝑣 ∈ 𝑉 ∃𝑤 ∈ (𝑉 ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ ∃𝑣 ∈ {𝐴, 𝐵, 𝐶}∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤}))
27	21, 26	syl 17	. 2 ⊢ (𝜑 → (∃𝑣 ∈ 𝑉 ∃𝑤 ∈ (𝑉 ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ ∃𝑣 ∈ {𝐴, 𝐵, 𝐶}∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤}))
28		preq2 4670	. . . . . . . 8 ⊢ (𝑤 = 𝐵 → {𝐴, 𝑤} = {𝐴, 𝐵})
29	28	eqeq2d 2749	. . . . . . 7 ⊢ (𝑤 = 𝐵 → ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵}))
30		preq2 4670	. . . . . . . 8 ⊢ (𝑤 = 𝐶 → {𝐴, 𝑤} = {𝐴, 𝐶})
31	30	eqeq2d 2749	. . . . . . 7 ⊢ (𝑤 = 𝐶 → ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}))
32	29, 31	rexprg 4632	. . . . . 6 ⊢ ((𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∃𝑤 ∈ {𝐵, 𝐶} (𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∨ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶})))
33	32	3adant1 1129	. . . . 5 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∃𝑤 ∈ {𝐵, 𝐶} (𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∨ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶})))
34		preq2 4670	. . . . . . . . 9 ⊢ (𝑤 = 𝐶 → {𝐵, 𝑤} = {𝐵, 𝐶})
35	34	eqeq2d 2749	. . . . . . . 8 ⊢ (𝑤 = 𝐶 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶}))
36		preq2 4670	. . . . . . . . 9 ⊢ (𝑤 = 𝐴 → {𝐵, 𝑤} = {𝐵, 𝐴})
37	36	eqeq2d 2749	. . . . . . . 8 ⊢ (𝑤 = 𝐴 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴}))
38	35, 37	rexprg 4632	. . . . . . 7 ⊢ ((𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋) → (∃𝑤 ∈ {𝐶, 𝐴} (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴})))
39	38	ancoms 459	. . . . . 6 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍) → (∃𝑤 ∈ {𝐶, 𝐴} (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴})))
40	39	3adant2 1130	. . . . 5 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∃𝑤 ∈ {𝐶, 𝐴} (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴})))
41		preq2 4670	. . . . . . . 8 ⊢ (𝑤 = 𝐴 → {𝐶, 𝑤} = {𝐶, 𝐴})
42	41	eqeq2d 2749	. . . . . . 7 ⊢ (𝑤 = 𝐴 → ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴}))
43		preq2 4670	. . . . . . . 8 ⊢ (𝑤 = 𝐵 → {𝐶, 𝑤} = {𝐶, 𝐵})
44	43	eqeq2d 2749	. . . . . . 7 ⊢ (𝑤 = 𝐵 → ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵}))
45	42, 44	rexprg 4632	. . . . . 6 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → (∃𝑤 ∈ {𝐴, 𝐵} (𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵})))
46	45	3adant3 1131	. . . . 5 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∃𝑤 ∈ {𝐴, 𝐵} (𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵})))
47	33, 40, 46	3orbi123d 1434	. . . 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 4685	. . . . . . . . 9 ⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴}
51	50	a1i 11	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴})
52	51	difeq1d 4056	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐴}) = ({𝐵, 𝐶, 𝐴} ∖ {𝐴}))
53		necom 2997	. . . . . . . . 9 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)
54		necom 2997	. . . . . . . . 9 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐶 ≠ 𝐴)
55		diftpsn3 4735	. . . . . . . . 9 ⊢ ((𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶})
56	53, 54, 55	syl2anb 598	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶})
57	56	3adant3 1131	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶})
58	52, 57	eqtrd 2778	. . . . . 6 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐴}) = {𝐵, 𝐶})
59	58	rexeqdv 3349	. . . . 5 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ↔ ∃𝑤 ∈ {𝐵, 𝐶} (𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤}))
60		tprot 4685	. . . . . . . . . 10 ⊢ {𝐶, 𝐴, 𝐵} = {𝐴, 𝐵, 𝐶}
61	60	eqcomi 2747	. . . . . . . . 9 ⊢ {𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵}
62	61	a1i 11	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → {𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵})
63	62	difeq1d 4056	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐵}) = ({𝐶, 𝐴, 𝐵} ∖ {𝐵}))
64		necom 2997	. . . . . . . . . . . 12 ⊢ (𝐵 ≠ 𝐶 ↔ 𝐶 ≠ 𝐵)
65	64	anbi1i 624	. . . . . . . . . . 11 ⊢ ((𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵) ↔ (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵))
66	65	biimpi 215	. . . . . . . . . 10 ⊢ ((𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵) → (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵))
67	66	ancoms 459	. . . . . . . . 9 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) → (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵))
68		diftpsn3 4735	. . . . . . . . 9 ⊢ ((𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴})
69	67, 68	syl 17	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴})
70	69	3adant2 1130	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴})
71	63, 70	eqtrd 2778	. . . . . 6 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐵}) = {𝐶, 𝐴})
72	71	rexeqdv 3349	. . . . 5 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ↔ ∃𝑤 ∈ {𝐶, 𝐴} (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤}))
73		diftpsn3 4735	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
74	73	3adant1 1129	. . . . . 6 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
75	74	rexeqdv 3349	. . . . 5 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤} ↔ ∃𝑤 ∈ {𝐴, 𝐵} (𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤}))
76	59, 72, 75	3orbi123d 1434	. . . 4 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ((∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤}) ↔ (∃𝑤 ∈ {𝐵, 𝐶} (𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ {𝐶, 𝐴} (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ {𝐴, 𝐵} (𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤})))
77	49, 76	syl 17	. . 3 ⊢ (𝜑 → ((∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤}) ↔ (∃𝑤 ∈ {𝐵, 𝐶} (𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ {𝐶, 𝐴} (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ {𝐴, 𝐵} (𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤})))
78		prcom 4668	. . . . . . . 8 ⊢ {𝐶, 𝐵} = {𝐵, 𝐶}
79	78	eqeq2i 2751	. . . . . . 7 ⊢ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵} ↔ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶})
80	79	orbi2i 910	. . . . . 6 ⊢ (((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵}) ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶}))
81		oridm 902	. . . . . 6 ⊢ (((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶}) ↔ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶})
82	80, 81	bitr2i 275	. . . . 5 ⊢ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵}))
83	82	a1i 11	. . . 4 ⊢ (𝜑 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵})))
84		nbgrnself2 27727	. . . . . . 7 ⊢ 𝐴 ∉ (𝐺 NeighbVtx 𝐴)
85		df-nel 3050	. . . . . . . 8 ⊢ (𝐴 ∉ (𝐺 NeighbVtx 𝐴) ↔ ¬ 𝐴 ∈ (𝐺 NeighbVtx 𝐴))
86		prid2g 4697	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝑋 → 𝐴 ∈ {𝐵, 𝐴})
87	86	3ad2ant1 1132	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → 𝐴 ∈ {𝐵, 𝐴})
88		eleq2 2827	. . . . . . . . . 10 ⊢ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴} → (𝐴 ∈ (𝐺 NeighbVtx 𝐴) ↔ 𝐴 ∈ {𝐵, 𝐴}))
89	87, 88	syl5ibrcom 246	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴} → 𝐴 ∈ (𝐺 NeighbVtx 𝐴)))
90	89	con3rr3 155	. . . . . . . 8 ⊢ (¬ 𝐴 ∈ (𝐺 NeighbVtx 𝐴) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ¬ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴}))
91	85, 90	sylbi 216	. . . . . . 7 ⊢ (𝐴 ∉ (𝐺 NeighbVtx 𝐴) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ¬ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴}))
92	84, 1, 91	mpsyl 68	. . . . . 6 ⊢ (𝜑 → ¬ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴})
93		biorf 934	. . . . . . 7 ⊢ (¬ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴} → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶})))
94		orcom 867	. . . . . . 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 4697	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝑋 → 𝐴 ∈ {𝐶, 𝐴})
98	97	3ad2ant1 1132	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → 𝐴 ∈ {𝐶, 𝐴})
99		eleq2 2827	. . . . . . . . . 10 ⊢ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} → (𝐴 ∈ (𝐺 NeighbVtx 𝐴) ↔ 𝐴 ∈ {𝐶, 𝐴}))
100	98, 99	syl5ibrcom 246	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} → 𝐴 ∈ (𝐺 NeighbVtx 𝐴)))
101	100	con3rr3 155	. . . . . . . 8 ⊢ (¬ 𝐴 ∈ (𝐺 NeighbVtx 𝐴) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ¬ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴}))
102	85, 101	sylbi 216	. . . . . . 7 ⊢ (𝐴 ∉ (𝐺 NeighbVtx 𝐴) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ¬ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴}))
103	84, 1, 102	mpsyl 68	. . . . . 6 ⊢ (𝜑 → ¬ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴})
104		biorf 934	. . . . . 6 ⊢ (¬ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} → ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵})))
105	103, 104	syl 17	. . . . 5 ⊢ (𝜑 → ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵})))
106	96, 105	orbi12d 916	. . . 4 ⊢ (𝜑 → (((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵}) ↔ (((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴}) ∨ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵}))))
107		prid1g 4696	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ 𝑋 → 𝐴 ∈ {𝐴, 𝐵})
108	107	3ad2ant1 1132	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → 𝐴 ∈ {𝐴, 𝐵})
109		eleq2 2827	. . . . . . . . . . . 12 ⊢ ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} → (𝐴 ∈ (𝐺 NeighbVtx 𝐴) ↔ 𝐴 ∈ {𝐴, 𝐵}))
110	108, 109	syl5ibrcom 246	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} → 𝐴 ∈ (𝐺 NeighbVtx 𝐴)))
111	110	con3dimp 409	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ ¬ 𝐴 ∈ (𝐺 NeighbVtx 𝐴)) → ¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵})
112		prid1g 4696	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ 𝑋 → 𝐴 ∈ {𝐴, 𝐶})
113	112	3ad2ant1 1132	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → 𝐴 ∈ {𝐴, 𝐶})
114		eleq2 2827	. . . . . . . . . . . 12 ⊢ ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶} → (𝐴 ∈ (𝐺 NeighbVtx 𝐴) ↔ 𝐴 ∈ {𝐴, 𝐶}))
115	113, 114	syl5ibrcom 246	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶} → 𝐴 ∈ (𝐺 NeighbVtx 𝐴)))
116	115	con3dimp 409	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ ¬ 𝐴 ∈ (𝐺 NeighbVtx 𝐴)) → ¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶})
117	111, 116	jca 512	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ ¬ 𝐴 ∈ (𝐺 NeighbVtx 𝐴)) → (¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∧ ¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}))
118	117	expcom 414	. . . . . . . 8 ⊢ (¬ 𝐴 ∈ (𝐺 NeighbVtx 𝐴) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∧ ¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶})))
119	85, 118	sylbi 216	. . . . . . 7 ⊢ (𝐴 ∉ (𝐺 NeighbVtx 𝐴) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∧ ¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶})))
120	84, 1, 119	mpsyl 68	. . . . . 6 ⊢ (𝜑 → (¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∧ ¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}))
121		ioran 981	. . . . . 6 ⊢ (¬ ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∨ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}) ↔ (¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∧ ¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}))
122	120, 121	sylibr 233	. . . . 5 ⊢ (𝜑 → ¬ ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∨ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}))
123	122	3bior1fd 1474	. . . 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 205   ∧ wa 396   ∨ wo 844   ∨ w3o 1085   ∧ w3a 1086   = wceq 1539   ∈ wcel 2106   ≠ wne 2943   ∉ wnel 3049  ∃wrex 3065   ∖ cdif 3884  {csn 4561  {cpr 4563  {ctp 4565  ‘cfv 6433  (class class class)co 7275  Vtxcvtx 27366  Edgcedg 27417  USGraphcusgr 27519   NeighbVtx cnbgr 27699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fv 6441  df-ov 7278  df-oprab 7279  df-mpo 7280  df-1st 7831  df-2nd 7832  df-nbgr 27700

This theorem is referenced by:  nb3grpr  27749