Theorem hasheni

Description: Equinumerous sets have the same number of elements (even if they are not finite). (Contributed by Mario Carneiro, 15-Apr-2015)

	Ref	Expression
Assertion	hasheni	⊢ ( 𝐴 ≈ 𝐵 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → 𝐴 ≈ 𝐵 )
2		enfii	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵 ) → 𝐴 ∈ Fin )
3	2	ancoms	⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → 𝐴 ∈ Fin )
4		hashen	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ↔ 𝐴 ≈ 𝐵 ) )
5	3 4	sylancom	⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ↔ 𝐴 ≈ 𝐵 ) )
6	1 5	mpbird	⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) )
7		relen	⊢ Rel ≈
8	7	brrelex1i	⊢ ( 𝐴 ≈ 𝐵 → 𝐴 ∈ V )
9		enfi	⊢ ( 𝐴 ≈ 𝐵 → ( 𝐴 ∈ Fin ↔ 𝐵 ∈ Fin ) )
10	9	notbid	⊢ ( 𝐴 ≈ 𝐵 → ( ¬ 𝐴 ∈ Fin ↔ ¬ 𝐵 ∈ Fin ) )
11	10	biimpar	⊢ ( ( 𝐴 ≈ 𝐵 ∧ ¬ 𝐵 ∈ Fin ) → ¬ 𝐴 ∈ Fin )
12		hashinf	⊢ ( ( 𝐴 ∈ V ∧ ¬ 𝐴 ∈ Fin ) → ( ♯ ‘ 𝐴 ) = +∞ )
13	8 11 12	syl2an2r	⊢ ( ( 𝐴 ≈ 𝐵 ∧ ¬ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐴 ) = +∞ )
14	7	brrelex2i	⊢ ( 𝐴 ≈ 𝐵 → 𝐵 ∈ V )
15		hashinf	⊢ ( ( 𝐵 ∈ V ∧ ¬ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐵 ) = +∞ )
16	14 15	sylan	⊢ ( ( 𝐴 ≈ 𝐵 ∧ ¬ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐵 ) = +∞ )
17	13 16	eqtr4d	⊢ ( ( 𝐴 ≈ 𝐵 ∧ ¬ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) )
18	6 17	pm2.61dan	⊢ ( 𝐴 ≈ 𝐵 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) )