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