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

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 ⊢ A ∈ V → card ⁡ A ∈ card ⁡ 𝒫 A

Proof

Step Hyp Ref Expression
1 canth2g ⊢ A ∈ V → A ≺ 𝒫 A
2 pwexg ⊢ A ∈ V → 𝒫 A ∈ V
3 cardsdom ⊢ A ∈ V ∧ 𝒫 A ∈ V → card ⁡ A ∈ card ⁡ 𝒫 A ↔ A ≺ 𝒫 A
4 2 3 mpdan ⊢ A ∈ V → card ⁡ A ∈ card ⁡ 𝒫 A ↔ A ≺ 𝒫 A
5 1 4 mpbird ⊢ A ∈ V → card ⁡ A ∈ card ⁡ 𝒫 A