This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 } )