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 ⊢ A ∈ dom ⁡ card → card ⁡ A = ∅ ↔ A = ∅

Proof

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