Description: The value of the cumulative hierarchy of sets function is a subset of its value at the successor. JFM CLASSES1 Th. 39. (Contributed by FL, 20-Apr-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | r1sssuc | |- ( A e. On -> ( R1 ` A ) C_ ( R1 ` suc A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | r1tr | |- Tr ( R1 ` A ) |
|
| 2 | dftr4 | |- ( Tr ( R1 ` A ) <-> ( R1 ` A ) C_ ~P ( R1 ` A ) ) |
|
| 3 | 1 2 | mpbi | |- ( R1 ` A ) C_ ~P ( R1 ` A ) |
| 4 | r1suc | |- ( A e. On -> ( R1 ` suc A ) = ~P ( R1 ` A ) ) |
|
| 5 | 3 4 | sseqtrrid | |- ( A e. On -> ( R1 ` A ) C_ ( R1 ` suc A ) ) |