nb3grprlem2 - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > nb3grprlem2		Structured version Visualization version GIF version

Theorem nb3grprlem2 40609

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

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

Colors of variables: wff setvar class

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 ‘cfv 5804 (class class class)co 6549 Vtxcvtx 25673 Edgcedga 25792 USGraph cusgr 40379 NeighbVtx cnbgr 40550

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-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-fal 1481 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-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-id 4953 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-iota 5768 df-fun 5806 df-fv 5812 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-1st 7059 df-2nd 7060 df-nbgr 40554

This theorem is referenced by: nb3grpr 40610

W3C validator