Theorem nb3graprlem2 25981

Description: Lemma 2 for nb3grapr 25982. (Contributed by Alexander van der Vekens, 17-Oct-2017.)

Assertion

Ref	Expression
nb3graprlem2	⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ↔ ∃𝑣 ∈ 𝑉 ∃𝑤 ∈ (𝑉 ∖ {𝑣})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤}))

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

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

Proof of Theorem nb3graprlem2

Step	Hyp	Ref	Expression
1		sneq 4135	. . . . . 6 ⊢ (𝑣 = 𝐴 → {𝑣} = {𝐴})
2	1	difeq2d 3690	. . . . 5 ⊢ (𝑣 = 𝐴 → ({𝐴, 𝐵, 𝐶} ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐴}))
3		preq1 4212	. . . . . 6 ⊢ (𝑣 = 𝐴 → {𝑣, 𝑤} = {𝐴, 𝑤})
4	3	eqeq2d 2620	. . . . 5 ⊢ (𝑣 = 𝐴 → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤} ↔ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤}))
5	2, 4	rexeqbidv 3130	. . . 4 ⊢ (𝑣 = 𝐴 → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤} ↔ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤}))
6		sneq 4135	. . . . . 6 ⊢ (𝑣 = 𝐵 → {𝑣} = {𝐵})
7	6	difeq2d 3690	. . . . 5 ⊢ (𝑣 = 𝐵 → ({𝐴, 𝐵, 𝐶} ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐵}))
8		preq1 4212	. . . . . 6 ⊢ (𝑣 = 𝐵 → {𝑣, 𝑤} = {𝐵, 𝑤})
9	8	eqeq2d 2620	. . . . 5 ⊢ (𝑣 = 𝐵 → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤} ↔ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤}))
10	7, 9	rexeqbidv 3130	. . . 4 ⊢ (𝑣 = 𝐵 → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤} ↔ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤}))
11		sneq 4135	. . . . . 6 ⊢ (𝑣 = 𝐶 → {𝑣} = {𝐶})
12	11	difeq2d 3690	. . . . 5 ⊢ (𝑣 = 𝐶 → ({𝐴, 𝐵, 𝐶} ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐶}))
13		preq1 4212	. . . . . 6 ⊢ (𝑣 = 𝐶 → {𝑣, 𝑤} = {𝐶, 𝑤})
14	13	eqeq2d 2620	. . . . 5 ⊢ (𝑣 = 𝐶 → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤} ↔ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤}))
15	12, 14	rexeqbidv 3130	. . . 4 ⊢ (𝑣 = 𝐶 → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤} ↔ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤}))
16	5, 10, 15	rextpg 4184	. . 3 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∃𝑣 ∈ {𝐴, 𝐵, 𝐶}∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤} ↔ (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤})))
17	16	3ad2ant1 1075	. 2 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (∃𝑣 ∈ {𝐴, 𝐵, 𝐶}∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤} ↔ (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤})))
18		simpl 472	. . . 4 ⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → 𝑉 = {𝐴, 𝐵, 𝐶})
19		difeq1 3683	. . . . . 6 ⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → (𝑉 ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝑣}))
20	19	adantr 480	. . . . 5 ⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → (𝑉 ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝑣}))
21	20	rexeqdv 3122	. . . 4 ⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → (∃𝑤 ∈ (𝑉 ∖ {𝑣})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤} ↔ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤}))
22	18, 21	rexeqbidv 3130	. . 3 ⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → (∃𝑣 ∈ 𝑉 ∃𝑤 ∈ (𝑉 ∖ {𝑣})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤} ↔ ∃𝑣 ∈ {𝐴, 𝐵, 𝐶}∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤}))
23	22	3ad2ant2 1076	. 2 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (∃𝑣 ∈ 𝑉 ∃𝑤 ∈ (𝑉 ∖ {𝑣})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤} ↔ ∃𝑣 ∈ {𝐴, 𝐵, 𝐶}∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤}))
24		preq2 4213	. . . . . . . 8 ⊢ (𝑤 = 𝐵 → {𝐴, 𝑤} = {𝐴, 𝐵})
25	24	eqeq2d 2620	. . . . . . 7 ⊢ (𝑤 = 𝐵 → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤} ↔ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵}))
26		preq2 4213	. . . . . . . 8 ⊢ (𝑤 = 𝐶 → {𝐴, 𝑤} = {𝐴, 𝐶})
27	26	eqeq2d 2620	. . . . . . 7 ⊢ (𝑤 = 𝐶 → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤} ↔ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶}))
28	25, 27	rexprg 4182	. . . . . 6 ⊢ ((𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∃𝑤 ∈ {𝐵, 𝐶} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤} ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶})))
29	28	3adant1 1072	. . . . 5 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∃𝑤 ∈ {𝐵, 𝐶} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤} ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶})))
30		preq2 4213	. . . . . . . . 9 ⊢ (𝑤 = 𝐶 → {𝐵, 𝑤} = {𝐵, 𝐶})
31	30	eqeq2d 2620	. . . . . . . 8 ⊢ (𝑤 = 𝐶 → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤} ↔ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶}))
32		preq2 4213	. . . . . . . . 9 ⊢ (𝑤 = 𝐴 → {𝐵, 𝑤} = {𝐵, 𝐴})
33	32	eqeq2d 2620	. . . . . . . 8 ⊢ (𝑤 = 𝐴 → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤} ↔ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴}))
34	31, 33	rexprg 4182	. . . . . . 7 ⊢ ((𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋) → (∃𝑤 ∈ {𝐶, 𝐴} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤} ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴})))
35	34	ancoms 468	. . . . . 6 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍) → (∃𝑤 ∈ {𝐶, 𝐴} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤} ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴})))
36	35	3adant2 1073	. . . . 5 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∃𝑤 ∈ {𝐶, 𝐴} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤} ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴})))
37		preq2 4213	. . . . . . . 8 ⊢ (𝑤 = 𝐴 → {𝐶, 𝑤} = {𝐶, 𝐴})
38	37	eqeq2d 2620	. . . . . . 7 ⊢ (𝑤 = 𝐴 → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤} ↔ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴}))
39		preq2 4213	. . . . . . . 8 ⊢ (𝑤 = 𝐵 → {𝐶, 𝑤} = {𝐶, 𝐵})
40	39	eqeq2d 2620	. . . . . . 7 ⊢ (𝑤 = 𝐵 → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤} ↔ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵}))
41	38, 40	rexprg 4182	. . . . . 6 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → (∃𝑤 ∈ {𝐴, 𝐵} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤} ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵})))
42	41	3adant3 1074	. . . . 5 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∃𝑤 ∈ {𝐴, 𝐵} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤} ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵})))
43	29, 36, 42	3orbi123d 1390	. . . 4 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((∃𝑤 ∈ {𝐵, 𝐶} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ {𝐶, 𝐴} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ {𝐴, 𝐵} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤}) ↔ (((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶}) ∨ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴}) ∨ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵}))))
44	43	3ad2ant1 1075	. . 3 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((∃𝑤 ∈ {𝐵, 𝐶} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ {𝐶, 𝐴} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ {𝐴, 𝐵} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤}) ↔ (((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶}) ∨ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴}) ∨ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵}))))
45		tprot 4228	. . . . . . . . 9 ⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴}
46	45	a1i 11	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴})
47	46	difeq1d 3689	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐴}) = ({𝐵, 𝐶, 𝐴} ∖ {𝐴}))
48		necom 2835	. . . . . . . . 9 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)
49		necom 2835	. . . . . . . . 9 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐶 ≠ 𝐴)
50		diftpsn3 4273	. . . . . . . . 9 ⊢ ((𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶})
51	48, 49, 50	syl2anb 495	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶})
52	51	3adant3 1074	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶})
53	47, 52	eqtrd 2644	. . . . . 6 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐴}) = {𝐵, 𝐶})
54	53	rexeqdv 3122	. . . . 5 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤} ↔ ∃𝑤 ∈ {𝐵, 𝐶} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤}))
55		tprot 4228	. . . . . . . . . 10 ⊢ {𝐶, 𝐴, 𝐵} = {𝐴, 𝐵, 𝐶}
56	55	eqcomi 2619	. . . . . . . . 9 ⊢ {𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵}
57	56	a1i 11	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → {𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵})
58	57	difeq1d 3689	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐵}) = ({𝐶, 𝐴, 𝐵} ∖ {𝐵}))
59		necom 2835	. . . . . . . . . . . 12 ⊢ (𝐵 ≠ 𝐶 ↔ 𝐶 ≠ 𝐵)
60	59	anbi1i 727	. . . . . . . . . . 11 ⊢ ((𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵) ↔ (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵))
61	60	biimpi 205	. . . . . . . . . 10 ⊢ ((𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵) → (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵))
62	61	ancoms 468	. . . . . . . . 9 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) → (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵))
63		diftpsn3 4273	. . . . . . . . 9 ⊢ ((𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴})
64	62, 63	syl 17	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴})
65	64	3adant2 1073	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴})
66	58, 65	eqtrd 2644	. . . . . 6 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐵}) = {𝐶, 𝐴})
67	66	rexeqdv 3122	. . . . 5 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤} ↔ ∃𝑤 ∈ {𝐶, 𝐴} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤}))
68		diftpsn3 4273	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
69	68	3adant1 1072	. . . . . 6 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
70	69	rexeqdv 3122	. . . . 5 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤} ↔ ∃𝑤 ∈ {𝐴, 𝐵} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤}))
71	54, 67, 70	3orbi123d 1390	. . . 4 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ((∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤}) ↔ (∃𝑤 ∈ {𝐵, 𝐶} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ {𝐶, 𝐴} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ {𝐴, 𝐵} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤})))
72	71	3ad2ant3 1077	. . 3 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤}) ↔ (∃𝑤 ∈ {𝐵, 𝐶} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ {𝐶, 𝐴} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ {𝐴, 𝐵} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤})))
73		prcom 4211	. . . . . . . 8 ⊢ {𝐶, 𝐵} = {𝐵, 𝐶}
74	73	eqeq2i 2622	. . . . . . 7 ⊢ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵} ↔ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶})
75	74	orbi2i 540	. . . . . 6 ⊢ (((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵}) ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶}))
76		oridm 535	. . . . . 6 ⊢ (((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶}) ↔ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶})
77	75, 76	bitr2i 264	. . . . 5 ⊢ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵}))
78	77	a1i 11	. . . 4 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵})))
79		nbgranself2 25965	. . . . . . . . . 10 ⊢ (𝑉 USGrph 𝐸 → 𝐴 ∉ (⟨𝑉, 𝐸⟩ Neighbors 𝐴))
80		df-nel 2783	. . . . . . . . . . 11 ⊢ (𝐴 ∉ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) ↔ ¬ 𝐴 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐴))
81		prid2g 4240	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ 𝑋 → 𝐴 ∈ {𝐵, 𝐴})
82	81	3ad2ant1 1075	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → 𝐴 ∈ {𝐵, 𝐴})
83		eleq2 2677	. . . . . . . . . . . . 13 ⊢ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴} → (𝐴 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) ↔ 𝐴 ∈ {𝐵, 𝐴}))
84	82, 83	syl5ibrcom 236	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴} → 𝐴 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐴)))
85	84	con3rr3 150	. . . . . . . . . . 11 ⊢ (¬ 𝐴 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴}))
86	80, 85	sylbi 206	. . . . . . . . . 10 ⊢ (𝐴 ∉ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴}))
87	79, 86	syl 17	. . . . . . . . 9 ⊢ (𝑉 USGrph 𝐸 → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴}))
88	87	adantl 481	. . . . . . . 8 ⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴}))
89	88	impcom 445	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴})
90	89	3adant3 1074	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴})
91		biorf 419	. . . . . . 7 ⊢ (¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴} → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶})))
92		orcom 401	. . . . . . 7 ⊢ (((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶}) ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴}))
93	91, 92	syl6bb 275	. . . . . 6 ⊢ (¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴} → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴})))
94	90, 93	syl 17	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴})))
95		prid2g 4240	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ 𝑋 → 𝐴 ∈ {𝐶, 𝐴})
96	95	3ad2ant1 1075	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → 𝐴 ∈ {𝐶, 𝐴})
97		eleq2 2677	. . . . . . . . . . . . 13 ⊢ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴} → (𝐴 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) ↔ 𝐴 ∈ {𝐶, 𝐴}))
98	96, 97	syl5ibrcom 236	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴} → 𝐴 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐴)))
99	98	con3rr3 150	. . . . . . . . . . 11 ⊢ (¬ 𝐴 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴}))
100	80, 99	sylbi 206	. . . . . . . . . 10 ⊢ (𝐴 ∉ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴}))
101	79, 100	syl 17	. . . . . . . . 9 ⊢ (𝑉 USGrph 𝐸 → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴}))
102	101	adantl 481	. . . . . . . 8 ⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴}))
103	102	impcom 445	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴})
104	103	3adant3 1074	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴})
105		biorf 419	. . . . . 6 ⊢ (¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴} → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵} ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵})))
106	104, 105	syl 17	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵} ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵})))
107	94, 106	orbi12d 742	. . . 4 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵}) ↔ (((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴}) ∨ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵}))))
108		prid1g 4239	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ 𝑋 → 𝐴 ∈ {𝐴, 𝐵})
109	108	3ad2ant1 1075	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → 𝐴 ∈ {𝐴, 𝐵})
110		eleq2 2677	. . . . . . . . . . . . . . 15 ⊢ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} → (𝐴 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) ↔ 𝐴 ∈ {𝐴, 𝐵}))
111	109, 110	syl5ibrcom 236	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} → 𝐴 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐴)))
112	111	con3dimp 456	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ ¬ 𝐴 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐴)) → ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵})
113		prid1g 4239	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ 𝑋 → 𝐴 ∈ {𝐴, 𝐶})
114	113	3ad2ant1 1075	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → 𝐴 ∈ {𝐴, 𝐶})
115		eleq2 2677	. . . . . . . . . . . . . . 15 ⊢ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶} → (𝐴 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) ↔ 𝐴 ∈ {𝐴, 𝐶}))
116	114, 115	syl5ibrcom 236	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶} → 𝐴 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐴)))
117	116	con3dimp 456	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ ¬ 𝐴 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐴)) → ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶})
118	112, 117	jca 553	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ ¬ 𝐴 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐴)) → (¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∧ ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶}))
119	118	expcom 450	. . . . . . . . . . 11 ⊢ (¬ 𝐴 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∧ ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶})))
120	80, 119	sylbi 206	. . . . . . . . . 10 ⊢ (𝐴 ∉ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∧ ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶})))
121	79, 120	syl 17	. . . . . . . . 9 ⊢ (𝑉 USGrph 𝐸 → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∧ ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶})))
122	121	adantl 481	. . . . . . . 8 ⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∧ ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶})))
123	122	impcom 445	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → (¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∧ ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶}))
124	123	3adant3 1074	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∧ ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶}))
125		ioran 510	. . . . . 6 ⊢ (¬ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶}) ↔ (¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∧ ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶}))
126	124, 125	sylibr 223	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ¬ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶}))
127	126	3bior1fd 1430	. . . 4 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴}) ∨ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵})) ↔ (((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶}) ∨ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴}) ∨ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵}))))
128	78, 107, 127	3bitrd 293	. . 3 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ↔ (((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶}) ∨ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴}) ∨ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵}))))
129	44, 72, 128	3bitr4rd 300	. 2 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ↔ (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤})))
130	17, 23, 129	3bitr4rd 300	1 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ↔ ∃𝑣 ∈ 𝑉 ∃𝑤 ∈ (𝑉 ∖ {𝑣})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤}))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∨ w3o 1030   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780   ∉ wnel 2781  ∃wrex 2897   ∖ cdif 3537  {csn 4125  {cpr 4127  {ctp 4129  ⟨cop 4131   class class class wbr 4583  (class class class)co 6549   USGrph cusg 25859   Neighbors cnbgra 25946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-hash 12980  df-usgra 25862  df-nbgra 25949

This theorem is referenced by:  nb3grapr  25982