Metamath Proof Explorer


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𝐴 = ∅ )