Metamath Proof Explorer


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 ( ¬ ∃* 𝑥 𝜑 ↔ ∀ 𝑦𝑥 ( 𝜑𝑥𝑦 ) )