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

Metamath Proof Explorer

Theorem carden2a

Description: If two sets have equal nonzero cardinalities, then they are equinumerous. This assertion and carden2b are meant to replace carden in ZF without AC. (Contributed by Mario Carneiro, 9-Jan-2013)

Ref Expression
Assertion carden2a ( ( ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ∧ ( card ‘ 𝐴 ) ≠ ∅ ) → 𝐴 ≈ 𝐵 )

Proof

Step Hyp Ref Expression
1 df-ne ⊢ ( ( card ‘ 𝐴 ) ≠ ∅ ↔ ¬ ( card ‘ 𝐴 ) = ∅ )
2 ndmfv ⊢ ( ¬ 𝐵 ∈ dom card → ( card ‘ 𝐵 ) = ∅ )
3 eqeq1 ⊢ ( ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) → ( ( card ‘ 𝐴 ) = ∅ ↔ ( card ‘ 𝐵 ) = ∅ ) )
4 2 3 imbitrrid ⊢ ( ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) → ( ¬ 𝐵 ∈ dom card → ( card ‘ 𝐴 ) = ∅ ) )
5 4 con1d ⊢ ( ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) → ( ¬ ( card ‘ 𝐴 ) = ∅ → 𝐵 ∈ dom card ) )
6 5 imp ⊢ ( ( ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ∧ ¬ ( card ‘ 𝐴 ) = ∅ ) → 𝐵 ∈ dom card )
7 cardid2 ⊢ ( 𝐵 ∈ dom card → ( card ‘ 𝐵 ) ≈ 𝐵 )
8 6 7 syl ⊢ ( ( ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ∧ ¬ ( card ‘ 𝐴 ) = ∅ ) → ( card ‘ 𝐵 ) ≈ 𝐵 )
9 breq2 ⊢ ( ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) → ( 𝐴 ≈ ( card ‘ 𝐴 ) ↔ 𝐴 ≈ ( card ‘ 𝐵 ) ) )
10 entr ⊢ ( ( 𝐴 ≈ ( card ‘ 𝐵 ) ∧ ( card ‘ 𝐵 ) ≈ 𝐵 ) → 𝐴 ≈ 𝐵 )
11 10 ex ⊢ ( 𝐴 ≈ ( card ‘ 𝐵 ) → ( ( card ‘ 𝐵 ) ≈ 𝐵 → 𝐴 ≈ 𝐵 ) )
12 9 11 biimtrdi ⊢ ( ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) → ( 𝐴 ≈ ( card ‘ 𝐴 ) → ( ( card ‘ 𝐵 ) ≈ 𝐵 → 𝐴 ≈ 𝐵 ) ) )
13 cardid2 ⊢ ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) ≈ 𝐴 )
14 ndmfv ⊢ ( ¬ 𝐴 ∈ dom card → ( card ‘ 𝐴 ) = ∅ )
15 13 14 nsyl4 ⊢ ( ¬ ( card ‘ 𝐴 ) = ∅ → ( card ‘ 𝐴 ) ≈ 𝐴 )
16 15 ensymd ⊢ ( ¬ ( card ‘ 𝐴 ) = ∅ → 𝐴 ≈ ( card ‘ 𝐴 ) )
17 12 16 impel ⊢ ( ( ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ∧ ¬ ( card ‘ 𝐴 ) = ∅ ) → ( ( card ‘ 𝐵 ) ≈ 𝐵 → 𝐴 ≈ 𝐵 ) )
18 8 17 mpd ⊢ ( ( ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ∧ ¬ ( card ‘ 𝐴 ) = ∅ ) → 𝐴 ≈ 𝐵 )
19 1 18 sylan2b ⊢ ( ( ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ∧ ( card ‘ 𝐴 ) ≠ ∅ ) → 𝐴 ≈ 𝐵 )