Step |
Hyp |
Ref |
Expression |
1 |
|
rankelun.1 |
|- A e. _V |
2 |
|
rankelun.2 |
|- B e. _V |
3 |
|
rankelun.3 |
|- C e. _V |
4 |
|
rankelun.4 |
|- D e. _V |
5 |
1 2 3 4
|
rankelpr |
|- ( ( ( rank ` A ) e. ( rank ` C ) /\ ( rank ` B ) e. ( rank ` D ) ) -> ( rank ` { A , B } ) e. ( rank ` { C , D } ) ) |
6 |
|
rankon |
|- ( rank ` { C , D } ) e. On |
7 |
6
|
onordi |
|- Ord ( rank ` { C , D } ) |
8 |
|
ordsucelsuc |
|- ( Ord ( rank ` { C , D } ) -> ( ( rank ` { A , B } ) e. ( rank ` { C , D } ) <-> suc ( rank ` { A , B } ) e. suc ( rank ` { C , D } ) ) ) |
9 |
7 8
|
ax-mp |
|- ( ( rank ` { A , B } ) e. ( rank ` { C , D } ) <-> suc ( rank ` { A , B } ) e. suc ( rank ` { C , D } ) ) |
10 |
5 9
|
sylib |
|- ( ( ( rank ` A ) e. ( rank ` C ) /\ ( rank ` B ) e. ( rank ` D ) ) -> suc ( rank ` { A , B } ) e. suc ( rank ` { C , D } ) ) |
11 |
1 2
|
rankop |
|- ( rank ` <. A , B >. ) = suc suc ( ( rank ` A ) u. ( rank ` B ) ) |
12 |
1 2
|
rankpr |
|- ( rank ` { A , B } ) = suc ( ( rank ` A ) u. ( rank ` B ) ) |
13 |
|
suceq |
|- ( ( rank ` { A , B } ) = suc ( ( rank ` A ) u. ( rank ` B ) ) -> suc ( rank ` { A , B } ) = suc suc ( ( rank ` A ) u. ( rank ` B ) ) ) |
14 |
12 13
|
ax-mp |
|- suc ( rank ` { A , B } ) = suc suc ( ( rank ` A ) u. ( rank ` B ) ) |
15 |
11 14
|
eqtr4i |
|- ( rank ` <. A , B >. ) = suc ( rank ` { A , B } ) |
16 |
3 4
|
rankop |
|- ( rank ` <. C , D >. ) = suc suc ( ( rank ` C ) u. ( rank ` D ) ) |
17 |
3 4
|
rankpr |
|- ( rank ` { C , D } ) = suc ( ( rank ` C ) u. ( rank ` D ) ) |
18 |
|
suceq |
|- ( ( rank ` { C , D } ) = suc ( ( rank ` C ) u. ( rank ` D ) ) -> suc ( rank ` { C , D } ) = suc suc ( ( rank ` C ) u. ( rank ` D ) ) ) |
19 |
17 18
|
ax-mp |
|- suc ( rank ` { C , D } ) = suc suc ( ( rank ` C ) u. ( rank ` D ) ) |
20 |
16 19
|
eqtr4i |
|- ( rank ` <. C , D >. ) = suc ( rank ` { C , D } ) |
21 |
10 15 20
|
3eltr4g |
|- ( ( ( rank ` A ) e. ( rank ` C ) /\ ( rank ` B ) e. ( rank ` D ) ) -> ( rank ` <. A , B >. ) e. ( rank ` <. C , D >. ) ) |