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