Description: Ordering relation for the cumulative hierarchy of sets. Part of Proposition 9.10(2) of TakeutiZaring p. 77. (Contributed by NM, 22-Sep-2003)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | r1ord2 | |- ( B e. On -> ( A e. B -> ( R1 ` A ) C_ ( R1 ` B ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | r1tr | |- Tr ( R1 ` B ) |
|
| 2 | r1ord | |- ( B e. On -> ( A e. B -> ( R1 ` A ) e. ( R1 ` B ) ) ) |
|
| 3 | trss | |- ( Tr ( R1 ` B ) -> ( ( R1 ` A ) e. ( R1 ` B ) -> ( R1 ` A ) C_ ( R1 ` B ) ) ) |
|
| 4 | 1 2 3 | mpsylsyld | |- ( B e. On -> ( A e. B -> ( R1 ` A ) C_ ( R1 ` B ) ) ) |