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

Metamath Proof Explorer

Theorem iscard3

Description: Two ways to express the property of being a cardinal number. (Contributed by NM, 9-Nov-2003)

Ref Expression
Assertion iscard3 
|- ( ( card ` A ) = A <-> A e. ( _om u. ran aleph ) )

Proof

Step Hyp Ref Expression
1 cardon 
 |-  ( card ` A ) e. On
2 eleq1 
 |-  ( ( card ` A ) = A -> ( ( card ` A ) e. On <-> A e. On ) )
3 1 2 mpbii 
 |-  ( ( card ` A ) = A -> A e. On )
4 eloni 
 |-  ( A e. On -> Ord A )
5 3 4 syl 
 |-  ( ( card ` A ) = A -> Ord A )
6 ordom 
 |-  Ord _om
7 ordtri2or 
 |-  ( ( Ord A /\ Ord _om ) -> ( A e. _om \/ _om C_ A ) )
8 5 6 7 sylancl 
 |-  ( ( card ` A ) = A -> ( A e. _om \/ _om C_ A ) )
9 8 ord 
 |-  ( ( card ` A ) = A -> ( -. A e. _om -> _om C_ A ) )
10 isinfcard 
 |-  ( ( _om C_ A /\ ( card ` A ) = A ) <-> A e. ran aleph )
11 10 biimpi 
 |-  ( ( _om C_ A /\ ( card ` A ) = A ) -> A e. ran aleph )
12 11 expcom 
 |-  ( ( card ` A ) = A -> ( _om C_ A -> A e. ran aleph ) )
13 9 12 syld 
 |-  ( ( card ` A ) = A -> ( -. A e. _om -> A e. ran aleph ) )
14 13 orrd 
 |-  ( ( card ` A ) = A -> ( A e. _om \/ A e. ran aleph ) )
15 cardnn 
 |-  ( A e. _om -> ( card ` A ) = A )
16 10 bicomi 
 |-  ( A e. ran aleph <-> ( _om C_ A /\ ( card ` A ) = A ) )
17 16 simprbi 
 |-  ( A e. ran aleph -> ( card ` A ) = A )
18 15 17 jaoi 
 |-  ( ( A e. _om \/ A e. ran aleph ) -> ( card ` A ) = A )
19 14 18 impbii 
 |-  ( ( card ` A ) = A <-> ( A e. _om \/ A e. ran aleph ) )
20 elun 
 |-  ( A e. ( _om u. ran aleph ) <-> ( A e. _om \/ A e. ran aleph ) )
21 19 20 bitr4i 
 |-  ( ( card ` A ) = A <-> A e. ( _om u. ran aleph ) )