This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZFC (ZERMELO-FRAENKEL WITH CHOICE) SET THEORY ZFC Set Theory - add the Axiom of Choice Cardinal number theorems using Axiom of Choice cardid
Description: Any set is equinumerous to its cardinal number. Proposition 10.5 of
TakeutiZaring p. 85. (Contributed by NM , 22-Oct-2003) (Revised by Mario Carneiro , 28-Apr-2015)
Ref
Expression
Hypothesis
cardval.1 ⊢ 𝐴 ∈ V
Assertion
cardid ⊢ ( card ‘ 𝐴 ) ≈ 𝐴
Proof
Step
Hyp
Ref
Expression
1
cardval.1 ⊢ 𝐴 ∈ V
2
numth3 ⊢ ( 𝐴 ∈ V → 𝐴 ∈ dom card )
3
cardid2 ⊢ ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) ≈ 𝐴 )
4
1 2 3
mp2b ⊢ ( card ‘ 𝐴 ) ≈ 𝐴