New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-spac GIF version

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 = (2cc x))}))
Distinct variable group:   x,m,y

Detailed syntax breakdown of Definition df-spac
StepHypRef Expression
1 cspac 6273 . 2 class Spac
2 vm . . 3 setvar m
3 cncs 6088 . . 3 class NC
42cv 1641 . . . . 5 class m
54csn 3737 . . . 4 class {m}
6 vx . . . . . . . 8 setvar x
76cv 1641 . . . . . . 7 class x
87, 3wcel 1710 . . . . . 6 wff x NC
9 vy . . . . . . . 8 setvar y
109cv 1641 . . . . . . 7 class y
1110, 3wcel 1710 . . . . . 6 wff y NC
12 c2c 6094 . . . . . . . 8 class 2c
13 cce 6096 . . . . . . . 8 class c
1412, 7, 13co 5525 . . . . . . 7 class (2cc x)
1510, 14wceq 1642 . . . . . 6 wff y = (2cc x)
168, 11, 15w3a 934 . . . . 5 wff (x NC y NC y = (2cc x))
1716, 6, 9copab 4622 . . . 4 class {x, y (x NC y NC y = (2cc x))}
185, 17cclos1 5872 . . 3 class Clos1 ({m}, {x, y (x NC y NC y = (2cc x))})
192, 3, 18cmpt 5651 . 2 class (m NC Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}))
201, 19wceq 1642 1 wff Spac = (m NC Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}))
 Colors of variables: wff setvar class This definition is referenced by:  spacval  6282  fnspac  6283
 Copyright terms: Public domain W3C validator