This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iotanul

Description: Theorem 8.22 in Quine p. 57. This theorem is the result if there isn't exactly one x that satisfies ph . (Contributed by Andrew Salmon, 11-Jul-2011)

Ref Expression
Assertion iotanul ⊢ ¬ ∃! x φ → ι x | φ = ∅

Proof

Step Hyp Ref Expression
1 eu6 ⊢ ∃! x φ ↔ ∃ z ∀ x φ ↔ x = z
2 dfiota2 ⊢ ι x | φ = ⋃ z | ∀ x φ ↔ x = z
3 alnex ⊢ ∀ z ¬ ∀ x φ ↔ x = z ↔ ¬ ∃ z ∀ x φ ↔ x = z
4 dfnul2 ⊢ ∅ = z | ¬ z = z
5 equid ⊢ z = z
6 5 tbt ⊢ ¬ ∀ x φ ↔ x = z ↔ ¬ ∀ x φ ↔ x = z ↔ z = z
7 6 biimpi ⊢ ¬ ∀ x φ ↔ x = z → ¬ ∀ x φ ↔ x = z ↔ z = z
8 7 con1bid ⊢ ¬ ∀ x φ ↔ x = z → ¬ z = z ↔ ∀ x φ ↔ x = z
9 8 alimi ⊢ ∀ z ¬ ∀ x φ ↔ x = z → ∀ z ¬ z = z ↔ ∀ x φ ↔ x = z
10 abbi ⊢ ∀ z ¬ z = z ↔ ∀ x φ ↔ x = z → z | ¬ z = z = z | ∀ x φ ↔ x = z
11 9 10 syl ⊢ ∀ z ¬ ∀ x φ ↔ x = z → z | ¬ z = z = z | ∀ x φ ↔ x = z
12 4 11 eqtr2id ⊢ ∀ z ¬ ∀ x φ ↔ x = z → z | ∀ x φ ↔ x = z = ∅
13 3 12 sylbir ⊢ ¬ ∃ z ∀ x φ ↔ x = z → z | ∀ x φ ↔ x = z = ∅
14 13 unieqd ⊢ ¬ ∃ z ∀ x φ ↔ x = z → ⋃ z | ∀ x φ ↔ x = z = ⋃ ∅
15 uni0 ⊢ ⋃ ∅ = ∅
16 14 15 eqtrdi ⊢ ¬ ∃ z ∀ x φ ↔ x = z → ⋃ z | ∀ x φ ↔ x = z = ∅
17 2 16 eqtrid ⊢ ¬ ∃ z ∀ x φ ↔ x = z → ι x | φ = ∅
18 1 17 sylnbi ⊢ ¬ ∃! x φ → ι x | φ = ∅