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