Definition df-cardn 3712

Description: Define the class of all cardinal numbers. The notation "Card" is used in Exercise 5(G) of [JustWeese] p. 174. It should not be confused with the lower-case "card" for the cardinal number function df-card 3623.

Assertion

Ref	Expression
df-cardn	⊢ Card = (ω ∪ ran ℵ)

Detailed syntax breakdown of Definition df-cardn

Step	Hyp	Ref	Expression
1		ccdn 3711	. 2 class Card
2		com 2372	. . 3 class ω
3		cale 3621	. . . 4 class ℵ
4	3	crn 2411	. . 3 class ran ℵ
5	2, 4	cun 1485	. 2 class (ω ∪ ran ℵ)
6	1, 5	wceq 1091	1 wff Card = (ω ∪ ran ℵ)

This definition is referenced by:  elcard 3713

metamath.org