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

Metamath Proof Explorer

Theorem cardnueq0

Description: The empty set is the only numerable set with cardinality zero. (Contributed by Mario Carneiro, 7-Jan-2013)

Ref Expression
Assertion cardnueq0 ( 𝐴 ∈ dom card → ( ( card ‘ 𝐴 ) = ∅ ↔ 𝐴 = ∅ ) )

Proof

Step Hyp Ref Expression
1 cardid2 ⊢ ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) ≈ 𝐴 )
2 1 ensymd ⊢ ( 𝐴 ∈ dom card → 𝐴 ≈ ( card ‘ 𝐴 ) )
3 breq2 ⊢ ( ( card ‘ 𝐴 ) = ∅ → ( 𝐴 ≈ ( card ‘ 𝐴 ) ↔ 𝐴 ≈ ∅ ) )
4 en0 ⊢ ( 𝐴 ≈ ∅ ↔ 𝐴 = ∅ )
5 3 4 bitrdi ⊢ ( ( card ‘ 𝐴 ) = ∅ → ( 𝐴 ≈ ( card ‘ 𝐴 ) ↔ 𝐴 = ∅ ) )
6 2 5 syl5ibcom ⊢ ( 𝐴 ∈ dom card → ( ( card ‘ 𝐴 ) = ∅ → 𝐴 = ∅ ) )
7 fveq2 ⊢ ( 𝐴 = ∅ → ( card ‘ 𝐴 ) = ( card ‘ ∅ ) )
8 card0 ⊢ ( card ‘ ∅ ) = ∅
9 7 8 eqtrdi ⊢ ( 𝐴 = ∅ → ( card ‘ 𝐴 ) = ∅ )
10 6 9 impbid1 ⊢ ( 𝐴 ∈ dom card → ( ( card ‘ 𝐴 ) = ∅ ↔ 𝐴 = ∅ ) )