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 ( ¬ ∃! 𝑥 𝜑 → ( ℩ 𝑥 𝜑 ) = ∅ )

Proof

Step Hyp Ref Expression
1 eu6 ⊢ ( ∃! 𝑥 𝜑 ↔ ∃ 𝑧 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) )
2 dfiota2 ⊢ ( ℩ 𝑥 𝜑 ) = ∪ { 𝑧 ∣ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) }
3 alnex ⊢ ( ∀ 𝑧 ¬ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ↔ ¬ ∃ 𝑧 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) )
4 dfnul2 ⊢ ∅ = { 𝑧 ∣ ¬ 𝑧 = 𝑧 }
5 equid ⊢ 𝑧 = 𝑧
6 5 tbt ⊢ ( ¬ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ↔ ( ¬ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ↔ 𝑧 = 𝑧 ) )
7 6 biimpi ⊢ ( ¬ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) → ( ¬ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ↔ 𝑧 = 𝑧 ) )
8 7 con1bid ⊢ ( ¬ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) → ( ¬ 𝑧 = 𝑧 ↔ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ) )
9 8 alimi ⊢ ( ∀ 𝑧 ¬ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) → ∀ 𝑧 ( ¬ 𝑧 = 𝑧 ↔ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ) )
10 abbi ⊢ ( ∀ 𝑧 ( ¬ 𝑧 = 𝑧 ↔ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ) → { 𝑧 ∣ ¬ 𝑧 = 𝑧 } = { 𝑧 ∣ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) } )
11 9 10 syl ⊢ ( ∀ 𝑧 ¬ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) → { 𝑧 ∣ ¬ 𝑧 = 𝑧 } = { 𝑧 ∣ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) } )
12 4 11 eqtr2id ⊢ ( ∀ 𝑧 ¬ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) → { 𝑧 ∣ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) } = ∅ )
13 3 12 sylbir ⊢ ( ¬ ∃ 𝑧 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) → { 𝑧 ∣ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) } = ∅ )
14 13 unieqd ⊢ ( ¬ ∃ 𝑧 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) → ∪ { 𝑧 ∣ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) } = ∪ ∅ )
15 uni0 ⊢ ∪ ∅ = ∅
16 14 15 eqtrdi ⊢ ( ¬ ∃ 𝑧 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) → ∪ { 𝑧 ∣ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) } = ∅ )
17 2 16 eqtrid ⊢ ( ¬ ∃ 𝑧 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) → ( ℩ 𝑥 𝜑 ) = ∅ )
18 1 17 sylnbi ⊢ ( ¬ ∃! 𝑥 𝜑 → ( ℩ 𝑥 𝜑 ) = ∅ )