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