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

Metamath Proof Explorer

Theorem mo0sn

Description: Two ways of expressing "at most one" element in a class. (Contributed by Zhi Wang, 19-Sep-2024)

Ref Expression
Assertion mo0sn ( ∃* 𝑥 𝑥 ∈ 𝐴 ↔ ( 𝐴 = ∅ ∨ ∃ 𝑦 𝐴 = { 𝑦 } ) )

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ 𝑧 𝑥 ∈ 𝐴
2 nfv ⊢ Ⅎ 𝑥 𝑧 ∈ 𝐴
3 eleq1w ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
4 1 2 3 cbvmow ⊢ ( ∃* 𝑥 𝑥 ∈ 𝐴 ↔ ∃* 𝑧 𝑧 ∈ 𝐴 )
5 neq0 ⊢ ( ¬ 𝐴 = ∅ ↔ ∃ 𝑧 𝑧 ∈ 𝐴 )
6 5 anbi1i ⊢ ( ( ¬ 𝐴 = ∅ ∧ ∃* 𝑧 𝑧 ∈ 𝐴 ) ↔ ( ∃ 𝑧 𝑧 ∈ 𝐴 ∧ ∃* 𝑧 𝑧 ∈ 𝐴 ) )
7 df-eu ⊢ ( ∃! 𝑧 𝑧 ∈ 𝐴 ↔ ( ∃ 𝑧 𝑧 ∈ 𝐴 ∧ ∃* 𝑧 𝑧 ∈ 𝐴 ) )
8 eu6 ⊢ ( ∃! 𝑧 𝑧 ∈ 𝐴 ↔ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝐴 ↔ 𝑧 = 𝑦 ) )
9 6 7 8 3bitr2i ⊢ ( ( ¬ 𝐴 = ∅ ∧ ∃* 𝑧 𝑧 ∈ 𝐴 ) ↔ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝐴 ↔ 𝑧 = 𝑦 ) )
10 dfcleq ⊢ ( 𝐴 = { 𝑦 } ↔ ∀ 𝑧 ( 𝑧 ∈ 𝐴 ↔ 𝑧 ∈ { 𝑦 } ) )
11 velsn ⊢ ( 𝑧 ∈ { 𝑦 } ↔ 𝑧 = 𝑦 )
12 11 bibi2i ⊢ ( ( 𝑧 ∈ 𝐴 ↔ 𝑧 ∈ { 𝑦 } ) ↔ ( 𝑧 ∈ 𝐴 ↔ 𝑧 = 𝑦 ) )
13 12 albii ⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝐴 ↔ 𝑧 ∈ { 𝑦 } ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝐴 ↔ 𝑧 = 𝑦 ) )
14 10 13 sylbbr ⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝐴 ↔ 𝑧 = 𝑦 ) → 𝐴 = { 𝑦 } )
15 14 eximi ⊢ ( ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝐴 ↔ 𝑧 = 𝑦 ) → ∃ 𝑦 𝐴 = { 𝑦 } )
16 9 15 sylbi ⊢ ( ( ¬ 𝐴 = ∅ ∧ ∃* 𝑧 𝑧 ∈ 𝐴 ) → ∃ 𝑦 𝐴 = { 𝑦 } )
17 16 expcom ⊢ ( ∃* 𝑧 𝑧 ∈ 𝐴 → ( ¬ 𝐴 = ∅ → ∃ 𝑦 𝐴 = { 𝑦 } ) )
18 17 orrd ⊢ ( ∃* 𝑧 𝑧 ∈ 𝐴 → ( 𝐴 = ∅ ∨ ∃ 𝑦 𝐴 = { 𝑦 } ) )
19 mo0 ⊢ ( 𝐴 = ∅ → ∃* 𝑧 𝑧 ∈ 𝐴 )
20 mosn ⊢ ( 𝐴 = { 𝑦 } → ∃* 𝑧 𝑧 ∈ 𝐴 )
21 20 exlimiv ⊢ ( ∃ 𝑦 𝐴 = { 𝑦 } → ∃* 𝑧 𝑧 ∈ 𝐴 )
22 19 21 jaoi ⊢ ( ( 𝐴 = ∅ ∨ ∃ 𝑦 𝐴 = { 𝑦 } ) → ∃* 𝑧 𝑧 ∈ 𝐴 )
23 18 22 impbii ⊢ ( ∃* 𝑧 𝑧 ∈ 𝐴 ↔ ( 𝐴 = ∅ ∨ ∃ 𝑦 𝐴 = { 𝑦 } ) )
24 4 23 bitri ⊢ ( ∃* 𝑥 𝑥 ∈ 𝐴 ↔ ( 𝐴 = ∅ ∨ ∃ 𝑦 𝐴 = { 𝑦 } ) )