Theorem sdom1

Description: A set has less than one member iff it is empty. (Contributed by Stefan O'Rear, 28-Oct-2014)

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

Proof

Step	Hyp	Ref	Expression
1		domnsym	⊢ ( 1o ≼ 𝐴 → ¬ 𝐴 ≺ 1o )
2	1	con2i	⊢ ( 𝐴 ≺ 1o → ¬ 1o ≼ 𝐴 )
3		0sdom1dom	⊢ ( ∅ ≺ 𝐴 ↔ 1o ≼ 𝐴 )
4	2 3	sylnibr	⊢ ( 𝐴 ≺ 1o → ¬ ∅ ≺ 𝐴 )
5		relsdom	⊢ Rel ≺
6	5	brrelex1i	⊢ ( 𝐴 ≺ 1o → 𝐴 ∈ V )
7		0sdomg	⊢ ( 𝐴 ∈ V → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) )
8	7	necon2bbid	⊢ ( 𝐴 ∈ V → ( 𝐴 = ∅ ↔ ¬ ∅ ≺ 𝐴 ) )
9	6 8	syl	⊢ ( 𝐴 ≺ 1o → ( 𝐴 = ∅ ↔ ¬ ∅ ≺ 𝐴 ) )
10	4 9	mpbird	⊢ ( 𝐴 ≺ 1o → 𝐴 = ∅ )
11		1n0	⊢ 1o ≠ ∅
12		1oex	⊢ 1o ∈ V
13	12	0sdom	⊢ ( ∅ ≺ 1o ↔ 1o ≠ ∅ )
14	11 13	mpbir	⊢ ∅ ≺ 1o
15		breq1	⊢ ( 𝐴 = ∅ → ( 𝐴 ≺ 1o ↔ ∅ ≺ 1o ) )
16	14 15	mpbiri	⊢ ( 𝐴 = ∅ → 𝐴 ≺ 1o )
17	10 16	impbii	⊢ ( 𝐴 ≺ 1o ↔ 𝐴 = ∅ )