Description: The union of a cumulative hierarchy of sets at ordinal A is a subset of the hierarchy at A . JFM CLASSES1 th. 40. (Contributed by FL, 20-Apr-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | r1tr2 | |- U. ( R1 ` A ) C_ ( R1 ` A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | r1tr | |- Tr ( R1 ` A ) |
|
| 2 | df-tr | |- ( Tr ( R1 ` A ) <-> U. ( R1 ` A ) C_ ( R1 ` A ) ) |
|
| 3 | 1 2 | mpbi | |- U. ( R1 ` A ) C_ ( R1 ` A ) |