Definition df-card

Description: Define the cardinal number function. The cardinal number of a set is the least ordinal number equinumerous to it. In other words, it is the "size" of the set. Definition of Enderton p. 197. See cardval for its value and cardval2 for a simpler version of its value. The principal theorem relating cardinality to equinumerosity is carden . Our notation is from Enderton. Other textbooks often use a double bar over the set to express this function. (Contributed by NM, 21-Oct-2003)

	Ref	Expression
Assertion	df-card	⊢ card = ( 𝑥 ∈ V ↦ ∩ { 𝑦 ∈ On ∣ 𝑦 ≈ 𝑥 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccrd	⊢ card
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		vy	⊢ 𝑦
4		con0	⊢ On
5	3	cv	⊢ 𝑦
6		cen	⊢ ≈
7	1	cv	⊢ 𝑥
8	5 7 6	wbr	⊢ 𝑦 ≈ 𝑥
9	8 3 4	crab	⊢ { 𝑦 ∈ On ∣ 𝑦 ≈ 𝑥 }
10	9	cint	⊢ ∩ { 𝑦 ∈ On ∣ 𝑦 ≈ 𝑥 }
11	1 2 10	cmpt	⊢ ( 𝑥 ∈ V ↦ ∩ { 𝑦 ∈ On ∣ 𝑦 ≈ 𝑥 } )
12	0 11	wceq	⊢ card = ( 𝑥 ∈ V ↦ ∩ { 𝑦 ∈ On ∣ 𝑦 ≈ 𝑥 } )