Theorem iscard

Description: Two ways to express the property of being a cardinal number. (Contributed by Mario Carneiro, 15-Jan-2013)

	Ref	Expression
Assertion	iscard	|- ( ( card ` A ) = A <-> ( A e. On /\ A. x e. A x ~< A ) )

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		cardonle	|- ( A e. On -> ( card ` A ) C_ A )
5		eqss	|- ( ( card ` A ) = A <-> ( ( card ` A ) C_ A /\ A C_ ( card ` A ) ) )
6	5	baibr	|- ( ( card ` A ) C_ A -> ( A C_ ( card ` A ) <-> ( card ` A ) = A ) )
7	4 6	syl	|- ( A e. On -> ( A C_ ( card ` A ) <-> ( card ` A ) = A ) )
8		dfss3	|- ( A C_ ( card ` A ) <-> A. x e. A x e. ( card ` A ) )
9		onelon	|- ( ( A e. On /\ x e. A ) -> x e. On )
10		onenon	|- ( A e. On -> A e. dom card )
11	10	adantr	|- ( ( A e. On /\ x e. A ) -> A e. dom card )
12		cardsdomel	|- ( ( x e. On /\ A e. dom card ) -> ( x ~< A <-> x e. ( card ` A ) ) )
13	9 11 12	syl2anc	|- ( ( A e. On /\ x e. A ) -> ( x ~< A <-> x e. ( card ` A ) ) )
14	13	ralbidva	|- ( A e. On -> ( A. x e. A x ~< A <-> A. x e. A x e. ( card ` A ) ) )
15	8 14	bitr4id	|- ( A e. On -> ( A C_ ( card ` A ) <-> A. x e. A x ~< A ) )
16	7 15	bitr3d	|- ( A e. On -> ( ( card ` A ) = A <-> A. x e. A x ~< A ) )
17	3 16	biadanii	|- ( ( card ` A ) = A <-> ( A e. On /\ A. x e. A x ~< A ) )