Metamath Proof Explorer


Theorem r1ord3

Description: Ordering relation for the cumulative hierarchy of sets. Part of Theorem 3.3(i) of BellMachover p. 478. (Contributed by NM, 22-Sep-2003)

Ref Expression
Assertion r1ord3
|- ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( R1 ` A ) C_ ( R1 ` B ) ) )

Proof

Step Hyp Ref Expression
1 r1fnon
 |-  R1 Fn On
2 1 fndmi
 |-  dom R1 = On
3 2 eleq2i
 |-  ( A e. dom R1 <-> A e. On )
4 2 eleq2i
 |-  ( B e. dom R1 <-> B e. On )
5 r1ord3g
 |-  ( ( A e. dom R1 /\ B e. dom R1 ) -> ( A C_ B -> ( R1 ` A ) C_ ( R1 ` B ) ) )
6 3 4 5 syl2anbr
 |-  ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( R1 ` A ) C_ ( R1 ` B ) ) )