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

Metamath Proof Explorer

Theorem alephprc

Description: The class of all transfinite cardinal numbers (the range of the aleph function) is a proper class. Proposition 10.26 of TakeutiZaring p. 90. (Contributed by NM, 11-Nov-2003)

Ref Expression
Assertion alephprc ⊢ ¬ ran ⁡ ℵ ∈ V

Proof

Step Hyp Ref Expression
1 cardprc ⊢ x | card ⁡ x = x ∉ V
2 1 neli ⊢ ¬ x | card ⁡ x = x ∈ V
3 cardnum ⊢ x | card ⁡ x = x = ω ∪ ran ⁡ ℵ
4 3 eleq1i ⊢ x | card ⁡ x = x ∈ V ↔ ω ∪ ran ⁡ ℵ ∈ V
5 2 4 mtbi ⊢ ¬ ω ∪ ran ⁡ ℵ ∈ V
6 omex ⊢ ω ∈ V
7 unexg ⊢ ω ∈ V ∧ ran ⁡ ℵ ∈ V → ω ∪ ran ⁡ ℵ ∈ V
8 6 7 mpan ⊢ ran ⁡ ℵ ∈ V → ω ∪ ran ⁡ ℵ ∈ V
9 5 8 mto ⊢ ¬ ran ⁡ ℵ ∈ V