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