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 ‘ 𝐴 ) ≠ ∅ ) → 𝐴 ≈ 𝐵 )