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

Metamath Proof Explorer

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 1 fndmi ⊢ dom 𝑅1 = On
3 2 eleq2i ⊢ ( 𝐴 ∈ dom 𝑅1 ↔ 𝐴 ∈ On )
4 r1val1 ⊢ ( 𝐴 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 𝒫 ( 𝑅1 ‘ 𝑥 ) )
5 3 4 sylbir ⊢ ( 𝐴 ∈ On → ( 𝑅1 ‘ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 𝒫 ( 𝑅1 ‘ 𝑥 ) )
6 onelon ⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ On )
7 r1val2 ⊢ ( 𝑥 ∈ On → ( 𝑅1 ‘ 𝑥 ) = { 𝑦 ∣ ( rank ‘ 𝑦 ) ∈ 𝑥 } )
8 6 7 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ 𝐴 ) → ( 𝑅1 ‘ 𝑥 ) = { 𝑦 ∣ ( rank ‘ 𝑦 ) ∈ 𝑥 } )
9 8 pweqd ⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ 𝐴 ) → 𝒫 ( 𝑅1 ‘ 𝑥 ) = 𝒫 { 𝑦 ∣ ( rank ‘ 𝑦 ) ∈ 𝑥 } )
10 9 iuneq2dv ⊢ ( 𝐴 ∈ On → ∪ 𝑥 ∈ 𝐴 𝒫 ( 𝑅1 ‘ 𝑥 ) = ∪ 𝑥 ∈ 𝐴 𝒫 { 𝑦 ∣ ( rank ‘ 𝑦 ) ∈ 𝑥 } )
11 5 10 eqtrd ⊢ ( 𝐴 ∈ On → ( 𝑅1 ‘ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 𝒫 { 𝑦 ∣ ( rank ‘ 𝑦 ) ∈ 𝑥 } )