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

Metamath Proof Explorer

Theorem card1

Description: A set has cardinality one iff it is a singleton. (Contributed by Mario Carneiro, 10-Jan-2013)

Ref Expression
Assertion card1 ( ( card ‘ 𝐴 ) = 1o ↔ ∃ 𝑥 𝐴 = { 𝑥 } )

Proof

Step Hyp Ref Expression
1 1onn ⊢ 1o ∈ ω
2 cardnn ⊢ ( 1o ∈ ω → ( card ‘ 1o ) = 1o )
3 1 2 ax-mp ⊢ ( card ‘ 1o ) = 1o
4 1n0 ⊢ 1o ≠ ∅
5 3 4 eqnetri ⊢ ( card ‘ 1o ) ≠ ∅
6 carden2a ⊢ ( ( ( card ‘ 1o ) = ( card ‘ 𝐴 ) ∧ ( card ‘ 1o ) ≠ ∅ ) → 1o ≈ 𝐴 )
7 5 6 mpan2 ⊢ ( ( card ‘ 1o ) = ( card ‘ 𝐴 ) → 1o ≈ 𝐴 )
8 7 eqcoms ⊢ ( ( card ‘ 𝐴 ) = ( card ‘ 1o ) → 1o ≈ 𝐴 )
9 8 ensymd ⊢ ( ( card ‘ 𝐴 ) = ( card ‘ 1o ) → 𝐴 ≈ 1o )
10 carden2b ⊢ ( 𝐴 ≈ 1o → ( card ‘ 𝐴 ) = ( card ‘ 1o ) )
11 9 10 impbii ⊢ ( ( card ‘ 𝐴 ) = ( card ‘ 1o ) ↔ 𝐴 ≈ 1o )
12 3 eqeq2i ⊢ ( ( card ‘ 𝐴 ) = ( card ‘ 1o ) ↔ ( card ‘ 𝐴 ) = 1o )
13 en1 ⊢ ( 𝐴 ≈ 1o ↔ ∃ 𝑥 𝐴 = { 𝑥 } )
14 11 12 13 3bitr3i ⊢ ( ( card ‘ 𝐴 ) = 1o ↔ ∃ 𝑥 𝐴 = { 𝑥 } )