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 AOnR1A=xA𝒫y|rankyx

Proof

Step Hyp Ref Expression
1 r1fnon R1FnOn
2 1 fndmi domR1=On
3 2 eleq2i AdomR1AOn
4 r1val1 AdomR1R1A=xA𝒫R1x
5 3 4 sylbir AOnR1A=xA𝒫R1x
6 onelon AOnxAxOn
7 r1val2 xOnR1x=y|rankyx
8 6 7 syl AOnxAR1x=y|rankyx
9 8 pweqd AOnxA𝒫R1x=𝒫y|rankyx
10 9 iuneq2dv AOnxA𝒫R1x=xA𝒫y|rankyx
11 5 10 eqtrd AOnR1A=xA𝒫y|rankyx