Description: A relationship between rank and R1 . See rankr1a for the membership version. (Contributed by NM, 15-Sep-2006) (Revised by Mario Carneiro, 17-Nov-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | rankr1b.1 | |- A e. _V |
|
| Assertion | rankr1b | |- ( B e. On -> ( A C_ ( R1 ` B ) <-> ( rank ` A ) C_ B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rankr1b.1 | |- A e. _V |
|
| 2 | r1fnon | |- R1 Fn On |
|
| 3 | 2 | fndmi | |- dom R1 = On |
| 4 | 3 | eleq2i | |- ( B e. dom R1 <-> B e. On ) |
| 5 | unir1 | |- U. ( R1 " On ) = _V |
|
| 6 | 1 5 | eleqtrri | |- A e. U. ( R1 " On ) |
| 7 | rankr1bg | |- ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( A C_ ( R1 ` B ) <-> ( rank ` A ) C_ B ) ) |
|
| 8 | 6 7 | mpan | |- ( B e. dom R1 -> ( A C_ ( R1 ` B ) <-> ( rank ` A ) C_ B ) ) |
| 9 | 4 8 | sylbir | |- ( B e. On -> ( A C_ ( R1 ` B ) <-> ( rank ` A ) C_ B ) ) |