Metamath Proof Explorer


Theorem rankelop

Description: Rank membership is inherited by ordered pairs. (Contributed by NM, 18-Sep-2006)

Ref Expression
Hypotheses rankelun.1
|- A e. _V
rankelun.2
|- B e. _V
rankelun.3
|- C e. _V
rankelun.4
|- D e. _V
Assertion rankelop
|- ( ( ( rank ` A ) e. ( rank ` C ) /\ ( rank ` B ) e. ( rank ` D ) ) -> ( rank ` <. A , B >. ) e. ( rank ` <. C , D >. ) )

Proof

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