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	⊢ ( ∃* 𝑥 𝑥 ∈ 𝐴 ↔ ( 𝐴 = ∅ ∨ ∃ 𝑦 𝐴 = { 𝑦 } ) )