This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ↔ 𝐴 ≈ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 carddom2 ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ↔ 𝐴 ≼ 𝐵 ) )
2 carddom2 ⊢ ( ( 𝐵 ∈ dom card ∧ 𝐴 ∈ dom card ) → ( ( card ‘ 𝐵 ) ⊆ ( card ‘ 𝐴 ) ↔ 𝐵 ≼ 𝐴 ) )
3 2 ancoms ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ 𝐵 ) ⊆ ( card ‘ 𝐴 ) ↔ 𝐵 ≼ 𝐴 ) )
4 1 3 anbi12d ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ∧ ( card ‘ 𝐵 ) ⊆ ( card ‘ 𝐴 ) ) ↔ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴 ) ) )
5 eqss ⊢ ( ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ↔ ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ∧ ( card ‘ 𝐵 ) ⊆ ( card ‘ 𝐴 ) ) )
6 5 bicomi ⊢ ( ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ∧ ( card ‘ 𝐵 ) ⊆ ( card ‘ 𝐴 ) ) ↔ ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) )
7 sbthb ⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴 ) ↔ 𝐴 ≈ 𝐵 )
8 4 6 7 3bitr3g ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ↔ 𝐴 ≈ 𝐵 ) )