Theorem sdom1

Description: A set has less than one member iff it is empty. (Contributed by Stefan O'Rear, 28-Oct-2014) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 12-Dec-2024)

	Ref	Expression
Assertion	sdom1	⊢ ( 𝐴 ≺ 1o ↔ 𝐴 = ∅ )

Proof

Step	Hyp	Ref	Expression
1		df1o2	⊢ 1o = { ∅ }
2	1	breq2i	⊢ ( 𝐴 ≼ 1o ↔ 𝐴 ≼ { ∅ } )
3		brdomi	⊢ ( 𝐴 ≼ { ∅ } → ∃ 𝑓 𝑓 : 𝐴 –1-1→ { ∅ } )
4		f1cdmsn	⊢ ( ( 𝑓 : 𝐴 –1-1→ { ∅ } ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 𝐴 = { 𝑥 } )
5		vex	⊢ 𝑥 ∈ V
6	5	ensn1	⊢ { 𝑥 } ≈ 1o
7		breq1	⊢ ( 𝐴 = { 𝑥 } → ( 𝐴 ≈ 1o ↔ { 𝑥 } ≈ 1o ) )
8	6 7	mpbiri	⊢ ( 𝐴 = { 𝑥 } → 𝐴 ≈ 1o )
9	8	exlimiv	⊢ ( ∃ 𝑥 𝐴 = { 𝑥 } → 𝐴 ≈ 1o )
10	4 9	syl	⊢ ( ( 𝑓 : 𝐴 –1-1→ { ∅ } ∧ 𝐴 ≠ ∅ ) → 𝐴 ≈ 1o )
11	10	expcom	⊢ ( 𝐴 ≠ ∅ → ( 𝑓 : 𝐴 –1-1→ { ∅ } → 𝐴 ≈ 1o ) )
12	11	exlimdv	⊢ ( 𝐴 ≠ ∅ → ( ∃ 𝑓 𝑓 : 𝐴 –1-1→ { ∅ } → 𝐴 ≈ 1o ) )
13	3 12	syl5	⊢ ( 𝐴 ≠ ∅ → ( 𝐴 ≼ { ∅ } → 𝐴 ≈ 1o ) )
14	2 13	biimtrid	⊢ ( 𝐴 ≠ ∅ → ( 𝐴 ≼ 1o → 𝐴 ≈ 1o ) )
15		iman	⊢ ( ( 𝐴 ≼ 1o → 𝐴 ≈ 1o ) ↔ ¬ ( 𝐴 ≼ 1o ∧ ¬ 𝐴 ≈ 1o ) )
16	14 15	sylib	⊢ ( 𝐴 ≠ ∅ → ¬ ( 𝐴 ≼ 1o ∧ ¬ 𝐴 ≈ 1o ) )
17		brsdom	⊢ ( 𝐴 ≺ 1o ↔ ( 𝐴 ≼ 1o ∧ ¬ 𝐴 ≈ 1o ) )
18	16 17	sylnibr	⊢ ( 𝐴 ≠ ∅ → ¬ 𝐴 ≺ 1o )
19	18	necon4ai	⊢ ( 𝐴 ≺ 1o → 𝐴 = ∅ )
20		1n0	⊢ 1o ≠ ∅
21		1oex	⊢ 1o ∈ V
22	21	0sdom	⊢ ( ∅ ≺ 1o ↔ 1o ≠ ∅ )
23	20 22	mpbir	⊢ ∅ ≺ 1o
24		breq1	⊢ ( 𝐴 = ∅ → ( 𝐴 ≺ 1o ↔ ∅ ≺ 1o ) )
25	23 24	mpbiri	⊢ ( 𝐴 = ∅ → 𝐴 ≺ 1o )
26	19 25	impbii	⊢ ( 𝐴 ≺ 1o ↔ 𝐴 = ∅ )