Theorem canth3

Description: Cantor's theorem in terms of cardinals. This theorem tells us that no matter how large a cardinal number is, there is a still larger cardinal number. Theorem 18.12 of Monk1 p. 133. (Contributed by NM, 5-Nov-2003)

	Ref	Expression
Assertion	canth3	|- ( A e. V -> ( card ` A ) e. ( card ` ~P A ) )

Proof

Step	Hyp	Ref	Expression
1		canth2g	|- ( A e. V -> A ~< ~P A )
2		pwexg	|- ( A e. V -> ~P A e. _V )
3		cardsdom	|- ( ( A e. V /\ ~P A e. _V ) -> ( ( card ` A ) e. ( card ` ~P A ) <-> A ~< ~P A ) )
4	2 3	mpdan	|- ( A e. V -> ( ( card ` A ) e. ( card ` ~P A ) <-> A ~< ~P A ) )
5	1 4	mpbird	|- ( A e. V -> ( card ` A ) e. ( card ` ~P A ) )