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 e. dom card -> ( ( card ` A ) = (/) <-> A = (/) ) )

Proof

Step Hyp Ref Expression
1 cardid2
 |-  ( A e. dom card -> ( card ` A ) ~~ A )
2 1 ensymd
 |-  ( A e. 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 e. 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 e. dom card -> ( ( card ` A ) = (/) <-> A = (/) ) )