Theorem ru 2643

Description: Russell's Paradox. Proposition 4.14 of [TakeutiZaring] p. 14.

In the late 1800s, Frege's Axiom of (unrestricted) Comprehension, expressed in our notation as A ∈ V, asserted that any collection of sets A is a set i.e. belongs to the universe V of all sets. In particular, by substituting {x ∣ x ∉ x} (the "Russell class") for A, it asserted {x ∣ x ∉ x} ∈ V, meaning that the "collection of all sets which are not members of themselves" is a set. However, here we prove {x ∣ x ∉ x} ∉ V. This contradiction was discovered by Russell in 1901 (published in 1903), invalidating the Comprehension Axiom and leading to the collapse of Frege's system.

In 1908, Zermelo rectified this fatal flaw by replacing Comprehension with a weaker Subset (or Separation) Axiom asserting that A is a set only when it is smaller than some other set B. The intuitionistic set theory IZF includes such a separation axiom, Axiom 6 of [Crosilla] p. "Axioms of CZF and IZF". (Contributed by NM, 7-Aug-1994.)

Assertion

Ref	Expression
ru	⊢ {x ∣ x ∉ x} ∉ V

Proof of Theorem ru

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		pm5.19 604	. . . . . 6 ⊢ ¬ (y ∈ y ↔ ¬ y ∈ y)
2		eleq1 2005	. . . . . . . 8 ⊢ (x = y → (x ∈ y ↔ y ∈ y))
3		df-nel 2110	. . . . . . . . 9 ⊢ (x ∉ x ↔ ¬ x ∈ x)
4		id 17	. . . . . . . . . . 11 ⊢ (x = y → x = y)
5	4, 4	eleq12d 2013	. . . . . . . . . 10 ⊢ (x = y → (x ∈ x ↔ y ∈ y))
6	5	notbid 574	. . . . . . . . 9 ⊢ (x = y → (¬ x ∈ x ↔ ¬ y ∈ y))
7	3, 6	syl5bb 179	. . . . . . . 8 ⊢ (x = y → (x ∉ x ↔ ¬ y ∈ y))
8	2, 7	bibi12d 222	. . . . . . 7 ⊢ (x = y → ((x ∈ y ↔ x ∉ x) ↔ (y ∈ y ↔ ¬ y ∈ y)))
9	8	spv 1679	. . . . . 6 ⊢ (∀x(x ∈ y ↔ x ∉ x) → (y ∈ y ↔ ¬ y ∈ y))
10	1, 9	mto 570	. . . . 5 ⊢ ¬ ∀x(x ∈ y ↔ x ∉ x)
11		abeq2 2050	. . . . 5 ⊢ (y = {x ∣ x ∉ x} ↔ ∀x(x ∈ y ↔ x ∉ x))
12	10, 11	mtbir 578	. . . 4 ⊢ ¬ y = {x ∣ x ∉ x}
13	12	nex 1336	. . 3 ⊢ ¬ ∃y y = {x ∣ x ∉ x}
14		isset 2445	. . 3 ⊢ ({x ∣ x ∉ x} ∈ V ↔ ∃y y = {x ∣ x ∉ x})
15	13, 14	mtbir 578	. 2 ⊢ ¬ {x ∣ x ∉ x} ∈ V
16		df-nel 2110	. 2 ⊢ ({x ∣ x ∉ x} ∉ V ↔ ¬ {x ∣ x ∉ x} ∈ V)
17	15, 16	mpbir 132	1 ⊢ {x ∣ x ∉ x} ∉ V

Syntax hints:  ¬ wn 3   ↔ wb 96  ∀wal 1281  ∃wex 1328   = wceq 1340   ∈ wcel 1342  {cab 1931   ∉ wnel 2108  Vcvv 2441

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 97  ax-ia2 98  ax-ia3 99  ax-in1 528  ax-in2 529  ax-5 1282  ax-7 1283  ax-gen 1284  ax-ie1 1329  ax-ie2 1330  ax-8 1344  ax-11 1346  ax-4 1349  ax-17 1367  ax-i9 1371  ax-ial 1376  ax-i5r 1377  ax-ext 1928

This theorem depends on definitions:  df-bi 108  df-tru 1204  df-fal 1205  df-nf 1296  df-sb 1586  df-clab 1932  df-cleq 1938  df-clel 1941  df-nel 2110  df-v 2443