Metamath Proof Explorer


Theorem r1ord2

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 ) ) )

Proof

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 ) ) )