Definition df-spac 6274

Description: Define the special class generator for the disproof of the axiom of choice. Definition 6.1 of [Specker] p. 973. (Contributed by SF, 3-Mar-2015.)

Assertion

Ref	Expression
df-spac	⊢ Spac = (m ∈ NC ↦ Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}))

Distinct variable group:   x,m,y

Detailed syntax breakdown of Definition df-spac

Step	Hyp	Ref	Expression
1		cspac 6273	. 2 class Spac
2		vm	. . 3 setvar m
3		cncs 6088	. . 3 class NC
4	2	cv 1641	. . . . 5 class m
5	4	csn 3737	. . . 4 class {m}
6		vx	. . . . . . . 8 setvar x
7	6	cv 1641	. . . . . . 7 class x
8	7, 3	wcel 1710	. . . . . 6 wff x ∈ NC
9		vy	. . . . . . . 8 setvar y
10	9	cv 1641	. . . . . . 7 class y
11	10, 3	wcel 1710	. . . . . 6 wff y ∈ NC
12		c2c 6094	. . . . . . . 8 class 2c
13		cce 6096	. . . . . . . 8 class ↑c
14	12, 7, 13	co 5525	. . . . . . 7 class (2c ↑c x)
15	10, 14	wceq 1642	. . . . . 6 wff y = (2c ↑c x)
16	8, 11, 15	w3a 934	. . . . 5 wff (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))
17	16, 6, 9	copab 4622	. . . 4 class {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}
18	5, 17	cclos1 5872	. . 3 class Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))})
19	2, 3, 18	cmpt 5651	. 2 class (m ∈ NC ↦ Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}))
20	1, 19	wceq 1642	1 wff Spac = (m ∈ NC ↦ Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}))

This definition is referenced by:  spacval  6282  fnspac  6283