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