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	⊢ ( 𝐴 ≈ 1o ↔ 𝐴 ∈ { 𝑥 ∣ ( card ‘ 𝑥 ) = 1o } )

Proof

Step	Hyp	Ref	Expression
1		carden2b	⊢ ( 𝐴 ≈ 1o → ( card ‘ 𝐴 ) = ( card ‘ 1o ) )
2		1onn	⊢ 1o ∈ ω
3		cardnn	⊢ ( 1o ∈ ω → ( card ‘ 1o ) = 1o )
4	2 3	ax-mp	⊢ ( card ‘ 1o ) = 1o
5	1 4	syl6eq	⊢ ( 𝐴 ≈ 1o → ( card ‘ 𝐴 ) = 1o )
6	4	eqeq2i	⊢ ( ( card ‘ 𝐴 ) = ( card ‘ 1o ) ↔ ( card ‘ 𝐴 ) = 1o )
7	6	biimpri	⊢ ( ( card ‘ 𝐴 ) = 1o → ( card ‘ 𝐴 ) = ( card ‘ 1o ) )
8		1n0	⊢ 1o ≠ ∅
9	8	neii	⊢ ¬ 1o = ∅
10		eqeq1	⊢ ( ( card ‘ 𝐴 ) = 1o → ( ( card ‘ 𝐴 ) = ∅ ↔ 1o = ∅ ) )
11	9 10	mtbiri	⊢ ( ( card ‘ 𝐴 ) = 1o → ¬ ( card ‘ 𝐴 ) = ∅ )
12		ndmfv	⊢ ( ¬ 𝐴 ∈ dom card → ( card ‘ 𝐴 ) = ∅ )
13	11 12	nsyl2	⊢ ( ( card ‘ 𝐴 ) = 1o → 𝐴 ∈ dom card )
14		1on	⊢ 1o ∈ On
15		onenon	⊢ ( 1o ∈ On → 1o ∈ dom card )
16	14 15	ax-mp	⊢ 1o ∈ dom card
17		carden2	⊢ ( ( 𝐴 ∈ dom card ∧ 1o ∈ dom card ) → ( ( card ‘ 𝐴 ) = ( card ‘ 1o ) ↔ 𝐴 ≈ 1o ) )
18	13 16 17	sylancl	⊢ ( ( card ‘ 𝐴 ) = 1o → ( ( card ‘ 𝐴 ) = ( card ‘ 1o ) ↔ 𝐴 ≈ 1o ) )
19	7 18	mpbid	⊢ ( ( card ‘ 𝐴 ) = 1o → 𝐴 ≈ 1o )
20	5 19	impbii	⊢ ( 𝐴 ≈ 1o ↔ ( card ‘ 𝐴 ) = 1o )
21	13	elexd	⊢ ( ( card ‘ 𝐴 ) = 1o → 𝐴 ∈ V )
22		fveqeq2	⊢ ( 𝑥 = 𝐴 → ( ( card ‘ 𝑥 ) = 1o ↔ ( card ‘ 𝐴 ) = 1o ) )
23	21 22	elab3	⊢ ( 𝐴 ∈ { 𝑥 ∣ ( card ‘ 𝑥 ) = 1o } ↔ ( card ‘ 𝐴 ) = 1o )
24	20 23	bitr4i	⊢ ( 𝐴 ≈ 1o ↔ 𝐴 ∈ { 𝑥 ∣ ( card ‘ 𝑥 ) = 1o } )