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