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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r1fnon | |
|
2 | 1 | fndmi | |
3 | 2 | eleq2i | |
4 | r1val1 | |
|
5 | 3 4 | sylbir | |
6 | onelon | |
|
7 | r1val2 | |
|
8 | 6 7 | syl | |
9 | 8 | pweqd | |
10 | 9 | iuneq2dv | |
11 | 5 10 | eqtrd | |