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