Theorem nmo

Description: Negation of "at most one". (Contributed by Thierry Arnoux, 26-Feb-2017)

	Ref	Expression
Hypothesis	nmo.1	⊢ Ⅎ 𝑦 𝜑
Assertion	nmo	⊢ ( ¬ ∃* 𝑥 𝜑 ↔ ∀ 𝑦 ∃ 𝑥 ( 𝜑 ∧ 𝑥 ≠ 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		nmo.1	⊢ Ⅎ 𝑦 𝜑
2	1	mof	⊢ ( ∃* 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
3	2	notbii	⊢ ( ¬ ∃* 𝑥 𝜑 ↔ ¬ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
4		alnex	⊢ ( ∀ 𝑦 ¬ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ↔ ¬ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
5		exnal	⊢ ( ∃ 𝑥 ¬ ( 𝜑 → 𝑥 = 𝑦 ) ↔ ¬ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
6		pm4.61	⊢ ( ¬ ( 𝜑 → 𝑥 = 𝑦 ) ↔ ( 𝜑 ∧ ¬ 𝑥 = 𝑦 ) )
7		biid	⊢ ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑦 )
8	7	necon3bbii	⊢ ( ¬ 𝑥 = 𝑦 ↔ 𝑥 ≠ 𝑦 )
9	8	anbi2i	⊢ ( ( 𝜑 ∧ ¬ 𝑥 = 𝑦 ) ↔ ( 𝜑 ∧ 𝑥 ≠ 𝑦 ) )
10	6 9	bitri	⊢ ( ¬ ( 𝜑 → 𝑥 = 𝑦 ) ↔ ( 𝜑 ∧ 𝑥 ≠ 𝑦 ) )
11	10	exbii	⊢ ( ∃ 𝑥 ¬ ( 𝜑 → 𝑥 = 𝑦 ) ↔ ∃ 𝑥 ( 𝜑 ∧ 𝑥 ≠ 𝑦 ) )
12	5 11	bitr3i	⊢ ( ¬ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ↔ ∃ 𝑥 ( 𝜑 ∧ 𝑥 ≠ 𝑦 ) )
13	12	albii	⊢ ( ∀ 𝑦 ¬ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ∃ 𝑥 ( 𝜑 ∧ 𝑥 ≠ 𝑦 ) )
14	3 4 13	3bitr2i	⊢ ( ¬ ∃* 𝑥 𝜑 ↔ ∀ 𝑦 ∃ 𝑥 ( 𝜑 ∧ 𝑥 ≠ 𝑦 ) )