Theorem r1val3

Description: The value of the cumulative hierarchy of sets function expressed in terms of rank. Theorem 15.18 of Monk1 p. 113. (Contributed by NM, 30-Nov-2003) (Revised by Mario Carneiro, 17-Nov-2014)

	Ref	Expression
Assertion	r1val3	⊢ ( 𝐴 ∈ On → ( 𝑅1 ‘ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 𝒫 { 𝑦 ∣ ( rank ‘ 𝑦 ) ∈ 𝑥 } )

Proof

Step	Hyp	Ref	Expression
1		r1fnon	⊢ 𝑅1 Fn On
2		fndm	⊢ ( 𝑅1 Fn On → dom 𝑅1 = On )
3	1 2	ax-mp	⊢ dom 𝑅1 = On
4	3	eleq2i	⊢ ( 𝐴 ∈ dom 𝑅1 ↔ 𝐴 ∈ On )
5		r1val1	⊢ ( 𝐴 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 𝒫 ( 𝑅1 ‘ 𝑥 ) )
6	4 5	sylbir	⊢ ( 𝐴 ∈ On → ( 𝑅1 ‘ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 𝒫 ( 𝑅1 ‘ 𝑥 ) )
7		onelon	⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ On )
8		r1val2	⊢ ( 𝑥 ∈ On → ( 𝑅1 ‘ 𝑥 ) = { 𝑦 ∣ ( rank ‘ 𝑦 ) ∈ 𝑥 } )
9	7 8	syl	⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ 𝐴 ) → ( 𝑅1 ‘ 𝑥 ) = { 𝑦 ∣ ( rank ‘ 𝑦 ) ∈ 𝑥 } )
10	9	pweqd	⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ 𝐴 ) → 𝒫 ( 𝑅1 ‘ 𝑥 ) = 𝒫 { 𝑦 ∣ ( rank ‘ 𝑦 ) ∈ 𝑥 } )
11	10	iuneq2dv	⊢ ( 𝐴 ∈ On → ∪ 𝑥 ∈ 𝐴 𝒫 ( 𝑅1 ‘ 𝑥 ) = ∪ 𝑥 ∈ 𝐴 𝒫 { 𝑦 ∣ ( rank ‘ 𝑦 ) ∈ 𝑥 } )
12	6 11	eqtrd	⊢ ( 𝐴 ∈ On → ( 𝑅1 ‘ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 𝒫 { 𝑦 ∣ ( rank ‘ 𝑦 ) ∈ 𝑥 } )