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 ~~ 1o <-> A e. { x | ( card ` x ) = 1o } )

Proof

Step	Hyp	Ref	Expression
1		carden2b	|- ( A ~~ 1o -> ( card ` A ) = ( card ` 1o ) )
2		1onn	|- 1o e. _om
3		cardnn	|- ( 1o e. _om -> ( card ` 1o ) = 1o )
4	2 3	ax-mp	|- ( card ` 1o ) = 1o
5	1 4	eqtrdi	|- ( A ~~ 1o -> ( card ` A ) = 1o )
6	4	eqeq2i	|- ( ( card ` A ) = ( card ` 1o ) <-> ( card ` A ) = 1o )
7	6	biimpri	|- ( ( card ` A ) = 1o -> ( card ` A ) = ( card ` 1o ) )
8		1n0	|- 1o =/= (/)
9	8	neii	|- -. 1o = (/)
10		eqeq1	|- ( ( card ` A ) = 1o -> ( ( card ` A ) = (/) <-> 1o = (/) ) )
11	9 10	mtbiri	|- ( ( card ` A ) = 1o -> -. ( card ` A ) = (/) )
12		ndmfv	|- ( -. A e. dom card -> ( card ` A ) = (/) )
13	11 12	nsyl2	|- ( ( card ` A ) = 1o -> A e. dom card )
14		1on	|- 1o e. On
15		onenon	|- ( 1o e. On -> 1o e. dom card )
16	14 15	ax-mp	|- 1o e. dom card
17		carden2	|- ( ( A e. dom card /\ 1o e. dom card ) -> ( ( card ` A ) = ( card ` 1o ) <-> A ~~ 1o ) )
18	13 16 17	sylancl	|- ( ( card ` A ) = 1o -> ( ( card ` A ) = ( card ` 1o ) <-> A ~~ 1o ) )
19	7 18	mpbid	|- ( ( card ` A ) = 1o -> A ~~ 1o )
20	5 19	impbii	|- ( A ~~ 1o <-> ( card ` A ) = 1o )
21		fveqeq2	|- ( x = A -> ( ( card ` x ) = 1o <-> ( card ` A ) = 1o ) )
22	13 21	elab3	|- ( A e. { x | ( card ` x ) = 1o } <-> ( card ` A ) = 1o )
23	20 22	bitr4i	|- ( A ~~ 1o <-> A e. { x | ( card ` x ) = 1o } )