Theorem pm54.43lem

Description: In Theorem *54.43 of WhiteheadRussell p. 360, the number 1 is defined as the collection of all sets with cardinality 1 (i.e. all singletons; see card1 ), so that their A e. 1 means, in our notation, A e. { x | ( cardx ) = 1o } . Here we show that this is equivalent to A ~1o so that we can use the latter more convenient notation in pm54.43 . (Contributed by NM, 4-Nov-2013)

	Ref	Expression
Assertion	pm54.43lem	$$⊢A\approx 1_{𝑜}\leftrightarrow A\in \left\{x|\mathrm{card}\left(x\right)=1_{𝑜}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		carden2b	$$⊢A\approx 1_{𝑜}\to \mathrm{card}\left(A\right)=\mathrm{card}\left(1_{𝑜}\right)$$
2		1onn	$$⊢1_{𝑜}\in \mathrm{\omega }$$
3		cardnn	$$⊢1_{𝑜}\in \mathrm{\omega }\to \mathrm{card}\left(1_{𝑜}\right)=1_{𝑜}$$
4	2 3	ax-mp	$$⊢\mathrm{card}\left(1_{𝑜}\right)=1_{𝑜}$$
5	1 4	eqtrdi	$$⊢A\approx 1_{𝑜}\to \mathrm{card}\left(A\right)=1_{𝑜}$$
6	4	eqeq2i	$$⊢\mathrm{card}\left(A\right)=\mathrm{card}\left(1_{𝑜}\right)\leftrightarrow \mathrm{card}\left(A\right)=1_{𝑜}$$
7	6	biimpri	$$⊢\mathrm{card}\left(A\right)=1_{𝑜}\to \mathrm{card}\left(A\right)=\mathrm{card}\left(1_{𝑜}\right)$$
8		1n0	$$⊢1_{𝑜}\ne \varnothing$$
9	8	neii	$$⊢\neg 1_{𝑜}=\varnothing$$
10		eqeq1	$$⊢\mathrm{card}\left(A\right)=1_{𝑜}\to \left(\mathrm{card}\left(A\right)=\varnothing \leftrightarrow 1_{𝑜}=\varnothing \right)$$
11	9 10	mtbiri	$$⊢\mathrm{card}\left(A\right)=1_{𝑜}\to \neg \mathrm{card}\left(A\right)=\varnothing$$
12		ndmfv	$$⊢\neg A\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left(A\right)=\varnothing$$
13	11 12	nsyl2	$$⊢\mathrm{card}\left(A\right)=1_{𝑜}\to A\in \mathrm{dom}\mathrm{card}$$
14		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
15		onenon	$$⊢1_{𝑜}\in \mathrm{On}\to 1_{𝑜}\in \mathrm{dom}\mathrm{card}$$
16	14 15	ax-mp	$$⊢1_{𝑜}\in \mathrm{dom}\mathrm{card}$$
17		carden2	$$⊢\left(A\in \mathrm{dom}\mathrm{card}\wedge 1_{𝑜}\in \mathrm{dom}\mathrm{card}\right)\to \left(\mathrm{card}\left(A\right)=\mathrm{card}\left(1_{𝑜}\right)\leftrightarrow A\approx 1_{𝑜}\right)$$
18	13 16 17	sylancl	$$⊢\mathrm{card}\left(A\right)=1_{𝑜}\to \left(\mathrm{card}\left(A\right)=\mathrm{card}\left(1_{𝑜}\right)\leftrightarrow A\approx 1_{𝑜}\right)$$
19	7 18	mpbid	$$⊢\mathrm{card}\left(A\right)=1_{𝑜}\to A\approx 1_{𝑜}$$
20	5 19	impbii	$$⊢A\approx 1_{𝑜}\leftrightarrow \mathrm{card}\left(A\right)=1_{𝑜}$$
21		fveqeq2	$$⊢x=A\to \left(\mathrm{card}\left(x\right)=1_{𝑜}\leftrightarrow \mathrm{card}\left(A\right)=1_{𝑜}\right)$$
22	13 21	elab3	$$⊢A\in \left\{x|\mathrm{card}\left(x\right)=1_{𝑜}\right\}\leftrightarrow \mathrm{card}\left(A\right)=1_{𝑜}$$
23	20 22	bitr4i	$$⊢A\approx 1_{𝑜}\leftrightarrow A\in \left\{x|\mathrm{card}\left(x\right)=1_{𝑜}\right\}$$