This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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