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	$$⊢A\approx B\to \left|A\right|=\left|B\right|$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(A\approx B\wedge B\in \mathrm{Fin}\right)\to A\approx B$$
2		enfii	$$⊢\left(B\in \mathrm{Fin}\wedge A\approx B\right)\to A\in \mathrm{Fin}$$
3	2	ancoms	$$⊢\left(A\approx B\wedge B\in \mathrm{Fin}\right)\to A\in \mathrm{Fin}$$
4		hashen	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left(\left|A\right|=\left|B\right|\leftrightarrow A\approx B\right)$$
5	3 4	sylancom	$$⊢\left(A\approx B\wedge B\in \mathrm{Fin}\right)\to \left(\left|A\right|=\left|B\right|\leftrightarrow A\approx B\right)$$
6	1 5	mpbird	$$⊢\left(A\approx B\wedge B\in \mathrm{Fin}\right)\to \left|A\right|=\left|B\right|$$
7		relen	$$⊢\mathrm{Rel}\approx$$
8	7	brrelex1i	$$⊢A\approx B\to A\in \mathrm{V}$$
9		enfi	$$⊢A\approx B\to \left(A\in \mathrm{Fin}\leftrightarrow B\in \mathrm{Fin}\right)$$
10	9	notbid	$$⊢A\approx B\to \left(\neg A\in \mathrm{Fin}\leftrightarrow \neg B\in \mathrm{Fin}\right)$$
11	10	biimpar	$$⊢\left(A\approx B\wedge \neg B\in \mathrm{Fin}\right)\to \neg A\in \mathrm{Fin}$$
12		hashinf	$$⊢\left(A\in \mathrm{V}\wedge \neg A\in \mathrm{Fin}\right)\to \left|A\right|=\mathrm{+\infty }$$
13	8 11 12	syl2an2r	$$⊢\left(A\approx B\wedge \neg B\in \mathrm{Fin}\right)\to \left|A\right|=\mathrm{+\infty }$$
14	7	brrelex2i	$$⊢A\approx B\to B\in \mathrm{V}$$
15		hashinf	$$⊢\left(B\in \mathrm{V}\wedge \neg B\in \mathrm{Fin}\right)\to \left|B\right|=\mathrm{+\infty }$$
16	14 15	sylan	$$⊢\left(A\approx B\wedge \neg B\in \mathrm{Fin}\right)\to \left|B\right|=\mathrm{+\infty }$$
17	13 16	eqtr4d	$$⊢\left(A\approx B\wedge \neg B\in \mathrm{Fin}\right)\to \left|A\right|=\left|B\right|$$
18	6 17	pm2.61dan	$$⊢A\approx B\to \left|A\right|=\left|B\right|$$