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

Metamath Proof Explorer

Theorem modom

Description: Two ways to express "at most one". (Contributed by Stefan O'Rear, 28-Oct-2014)

Ref Expression
Assertion modom ( ∃* 𝑥 𝜑 ↔ { 𝑥 ∣ 𝜑 } ≼ 1o )

Proof

Step Hyp Ref Expression
1 moeu ⊢ ( ∃* 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) )
2 imor ⊢ ( ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) ↔ ( ¬ ∃ 𝑥 𝜑 ∨ ∃! 𝑥 𝜑 ) )
3 abn0 ⊢ ( { 𝑥 ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑥 𝜑 )
4 3 necon1bbii ⊢ ( ¬ ∃ 𝑥 𝜑 ↔ { 𝑥 ∣ 𝜑 } = ∅ )
5 sdom1 ⊢ ( { 𝑥 ∣ 𝜑 } ≺ 1o ↔ { 𝑥 ∣ 𝜑 } = ∅ )
6 4 5 bitr4i ⊢ ( ¬ ∃ 𝑥 𝜑 ↔ { 𝑥 ∣ 𝜑 } ≺ 1o )
7 euen1 ⊢ ( ∃! 𝑥 𝜑 ↔ { 𝑥 ∣ 𝜑 } ≈ 1o )
8 6 7 orbi12i ⊢ ( ( ¬ ∃ 𝑥 𝜑 ∨ ∃! 𝑥 𝜑 ) ↔ ( { 𝑥 ∣ 𝜑 } ≺ 1o ∨ { 𝑥 ∣ 𝜑 } ≈ 1o ) )
9 brdom2 ⊢ ( { 𝑥 ∣ 𝜑 } ≼ 1o ↔ ( { 𝑥 ∣ 𝜑 } ≺ 1o ∨ { 𝑥 ∣ 𝜑 } ≈ 1o ) )
10 8 9 bitr4i ⊢ ( ( ¬ ∃ 𝑥 𝜑 ∨ ∃! 𝑥 𝜑 ) ↔ { 𝑥 ∣ 𝜑 } ≼ 1o )
11 1 2 10 3bitri ⊢ ( ∃* 𝑥 𝜑 ↔ { 𝑥 ∣ 𝜑 } ≼ 1o )