Metamath Proof Explorer


Theorem r1ord

Description: Ordering relation for the cumulative hierarchy of sets. Part of Proposition 9.10(2) of TakeutiZaring p. 77. (Contributed by NM, 8-Sep-2003) (Revised by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion r1ord
|- ( B e. On -> ( A e. B -> ( R1 ` A ) e. ( R1 ` B ) ) )

Proof

Step Hyp Ref Expression
1 r1fnon
 |-  R1 Fn On
2 1 fndmi
 |-  dom R1 = On
3 2 eleq2i
 |-  ( B e. dom R1 <-> B e. On )
4 r1ordg
 |-  ( B e. dom R1 -> ( A e. B -> ( R1 ` A ) e. ( R1 ` B ) ) )
5 3 4 sylbir
 |-  ( B e. On -> ( A e. B -> ( R1 ` A ) e. ( R1 ` B ) ) )