Metamath Proof Explorer


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 AVcardAcard𝒫A

Proof

Step Hyp Ref Expression
1 canth2g AVA𝒫A
2 pwexg AV𝒫AV
3 cardsdom AV𝒫AVcardAcard𝒫AA𝒫A
4 2 3 mpdan AVcardAcard𝒫AA𝒫A
5 1 4 mpbird AVcardAcard𝒫A