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