Metamath Proof Explorer

Theorem carden2

Description: Two numerable sets are equinumerous iff their cardinal numbers are equal. Unlike carden , the Axiom of Choice is not required. (Contributed by Mario Carneiro, 22-Sep-2013)

Ref Expression
Assertion carden2 ⊢A∈dom⁡card∧B∈dom⁡card→card⁡A=card⁡B↔A≈B

Proof

Step Hyp Ref Expression
1 carddom2 ⊢A∈dom⁡card∧B∈dom⁡card→card⁡A⊆card⁡B↔A≼B
2 carddom2 ⊢B∈dom⁡card∧A∈dom⁡card→card⁡B⊆card⁡A↔B≼A
3 2 ancoms ⊢A∈dom⁡card∧B∈dom⁡card→card⁡B⊆card⁡A↔B≼A
4 1 3 anbi12d ⊢A∈dom⁡card∧B∈dom⁡card→card⁡A⊆card⁡B∧card⁡B⊆card⁡A↔A≼B∧B≼A
5 eqss ⊢card⁡A=card⁡B↔card⁡A⊆card⁡B∧card⁡B⊆card⁡A
6 5 bicomi ⊢card⁡A⊆card⁡B∧card⁡B⊆card⁡A↔card⁡A=card⁡B
7 sbthb ⊢A≼B∧B≼A↔A≈B
8 4 6 7 3bitr3g ⊢A∈dom⁡card∧B∈dom⁡card→card⁡A=card⁡B↔A≈B