df-rank

Description: Define the rank function. See rankval , rankval2 , rankval3 , or rankval4 its value. The rank is a kind of "inverse" of the cumulative hierarchy of sets function R1 : given a set, it returns an ordinal number telling us the smallest layer of the hierarchy to which the set belongs. Based on Definition 9.14 of TakeutiZaring p. 79. Theorem rankid illustrates the "inverse" concept. Another nice theorem showing the relationship is rankr1a . (Contributed by NM, 11-Oct-2003)

		Ref	Expression
	Assertion	df-rank	⊢ rank = ( 𝑥 ∈ V ↦ ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅₁ ‘ suc 𝑦 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crnk	⊢ rank
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		vy	⊢ 𝑦
4		con0	⊢ On
5	1	cv	⊢ 𝑥
6		cr1	⊢ 𝑅₁
7	3	cv	⊢ 𝑦
8	7	csuc	⊢ suc 𝑦
9	8 6	cfv	⊢ ( 𝑅₁ ‘ suc 𝑦 )
10	5 9	wcel	⊢ 𝑥 ∈ ( 𝑅₁ ‘ suc 𝑦 )
11	10 3 4	crab	⊢ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅₁ ‘ suc 𝑦 ) }
12	11	cint	⊢ ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅₁ ‘ suc 𝑦 ) }
13	1 2 12	cmpt	⊢ ( 𝑥 ∈ V ↦ ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅₁ ‘ suc 𝑦 ) } )
14	0 13	wceq	⊢ rank = ( 𝑥 ∈ V ↦ ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅₁ ‘ suc 𝑦 ) } )

Metamath Proof Explorer

Definition df-rank

Detailed syntax breakdown