Metamath Proof Explorer


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 eqtrdi ( 𝐴 ≈ 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 fveqeq2 ( 𝑥 = 𝐴 → ( ( card ‘ 𝑥 ) = 1o ↔ ( card ‘ 𝐴 ) = 1o ) )
22 13 21 elab3 ( 𝐴 ∈ { 𝑥 ∣ ( card ‘ 𝑥 ) = 1o } ↔ ( card ‘ 𝐴 ) = 1o )
23 20 22 bitr4i ( 𝐴 ≈ 1o𝐴 ∈ { 𝑥 ∣ ( card ‘ 𝑥 ) = 1o } )