Theorem carden2b

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

	Ref	Expression
Assertion	carden2b	$$⊢A\approx B\to \mathrm{card}\left(A\right)=\mathrm{card}\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		cardne	$$⊢\mathrm{card}\left(B\right)\in \mathrm{card}\left(A\right)\to \neg \mathrm{card}\left(B\right)\approx A$$
2		ennum	$$⊢A\approx B\to \left(A\in \mathrm{dom}\mathrm{card}\leftrightarrow B\in \mathrm{dom}\mathrm{card}\right)$$
3	2	biimpa	$$⊢\left(A\approx B\wedge A\in \mathrm{dom}\mathrm{card}\right)\to B\in \mathrm{dom}\mathrm{card}$$
4		cardid2	$$⊢B\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left(B\right)\approx B$$
5	3 4	syl	$$⊢\left(A\approx B\wedge A\in \mathrm{dom}\mathrm{card}\right)\to \mathrm{card}\left(B\right)\approx B$$
6		ensym	$$⊢A\approx B\to B\approx A$$
7	6	adantr	$$⊢\left(A\approx B\wedge A\in \mathrm{dom}\mathrm{card}\right)\to B\approx A$$
8		entr	$$⊢\left(\mathrm{card}\left(B\right)\approx B\wedge B\approx A\right)\to \mathrm{card}\left(B\right)\approx A$$
9	5 7 8	syl2anc	$$⊢\left(A\approx B\wedge A\in \mathrm{dom}\mathrm{card}\right)\to \mathrm{card}\left(B\right)\approx A$$
10	1 9	nsyl3	$$⊢\left(A\approx B\wedge A\in \mathrm{dom}\mathrm{card}\right)\to \neg \mathrm{card}\left(B\right)\in \mathrm{card}\left(A\right)$$
11		cardon	$$⊢\mathrm{card}\left(A\right)\in \mathrm{On}$$
12		cardon	$$⊢\mathrm{card}\left(B\right)\in \mathrm{On}$$
13		ontri1	$$⊢\left(\mathrm{card}\left(A\right)\in \mathrm{On}\wedge \mathrm{card}\left(B\right)\in \mathrm{On}\right)\to \left(\mathrm{card}\left(A\right)\subseteq \mathrm{card}\left(B\right)\leftrightarrow \neg \mathrm{card}\left(B\right)\in \mathrm{card}\left(A\right)\right)$$
14	11 12 13	mp2an	$$⊢\mathrm{card}\left(A\right)\subseteq \mathrm{card}\left(B\right)\leftrightarrow \neg \mathrm{card}\left(B\right)\in \mathrm{card}\left(A\right)$$
15	10 14	sylibr	$$⊢\left(A\approx B\wedge A\in \mathrm{dom}\mathrm{card}\right)\to \mathrm{card}\left(A\right)\subseteq \mathrm{card}\left(B\right)$$
16		cardne	$$⊢\mathrm{card}\left(A\right)\in \mathrm{card}\left(B\right)\to \neg \mathrm{card}\left(A\right)\approx B$$
17		cardid2	$$⊢A\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left(A\right)\approx A$$
18		id	$$⊢A\approx B\to A\approx B$$
19		entr	$$⊢\left(\mathrm{card}\left(A\right)\approx A\wedge A\approx B\right)\to \mathrm{card}\left(A\right)\approx B$$
20	17 18 19	syl2anr	$$⊢\left(A\approx B\wedge A\in \mathrm{dom}\mathrm{card}\right)\to \mathrm{card}\left(A\right)\approx B$$
21	16 20	nsyl3	$$⊢\left(A\approx B\wedge A\in \mathrm{dom}\mathrm{card}\right)\to \neg \mathrm{card}\left(A\right)\in \mathrm{card}\left(B\right)$$
22		ontri1	$$⊢\left(\mathrm{card}\left(B\right)\in \mathrm{On}\wedge \mathrm{card}\left(A\right)\in \mathrm{On}\right)\to \left(\mathrm{card}\left(B\right)\subseteq \mathrm{card}\left(A\right)\leftrightarrow \neg \mathrm{card}\left(A\right)\in \mathrm{card}\left(B\right)\right)$$
23	12 11 22	mp2an	$$⊢\mathrm{card}\left(B\right)\subseteq \mathrm{card}\left(A\right)\leftrightarrow \neg \mathrm{card}\left(A\right)\in \mathrm{card}\left(B\right)$$
24	21 23	sylibr	$$⊢\left(A\approx B\wedge A\in \mathrm{dom}\mathrm{card}\right)\to \mathrm{card}\left(B\right)\subseteq \mathrm{card}\left(A\right)$$
25	15 24	eqssd	$$⊢\left(A\approx B\wedge A\in \mathrm{dom}\mathrm{card}\right)\to \mathrm{card}\left(A\right)=\mathrm{card}\left(B\right)$$
26		ndmfv	$$⊢\neg A\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left(A\right)=\varnothing$$
27	26	adantl	$$⊢\left(A\approx B\wedge \neg A\in \mathrm{dom}\mathrm{card}\right)\to \mathrm{card}\left(A\right)=\varnothing$$
28	2	notbid	$$⊢A\approx B\to \left(\neg A\in \mathrm{dom}\mathrm{card}\leftrightarrow \neg B\in \mathrm{dom}\mathrm{card}\right)$$
29	28	biimpa	$$⊢\left(A\approx B\wedge \neg A\in \mathrm{dom}\mathrm{card}\right)\to \neg B\in \mathrm{dom}\mathrm{card}$$
30		ndmfv	$$⊢\neg B\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left(B\right)=\varnothing$$
31	29 30	syl	$$⊢\left(A\approx B\wedge \neg A\in \mathrm{dom}\mathrm{card}\right)\to \mathrm{card}\left(B\right)=\varnothing$$
32	27 31	eqtr4d	$$⊢\left(A\approx B\wedge \neg A\in \mathrm{dom}\mathrm{card}\right)\to \mathrm{card}\left(A\right)=\mathrm{card}\left(B\right)$$
33	25 32	pm2.61dan	$$⊢A\approx B\to \mathrm{card}\left(A\right)=\mathrm{card}\left(B\right)$$