This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rankelpr

Description: Rank membership is inherited by unordered pairs. (Contributed by NM, 18-Sep-2006) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Hypotheses rankelun.1 
|- A e. _V
rankelun.2 
|- B e. _V
rankelun.3 
|- C e. _V
rankelun.4 
|- D e. _V
Assertion rankelpr 
|- ( ( ( 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 rankelun 
 |-  ( ( ( rank ` A ) e. ( rank ` C ) /\ ( rank ` B ) e. ( rank ` D ) ) -> ( rank ` ( A u. B ) ) e. ( rank ` ( C u. D ) ) )
6 1 2 rankun 
 |-  ( rank ` ( A u. B ) ) = ( ( rank ` A ) u. ( rank ` B ) )
7 3 4 rankun 
 |-  ( rank ` ( C u. D ) ) = ( ( rank ` C ) u. ( rank ` D ) )
8 5 6 7 3eltr3g 
 |-  ( ( ( rank ` A ) e. ( rank ` C ) /\ ( rank ` B ) e. ( rank ` D ) ) -> ( ( rank ` A ) u. ( rank ` B ) ) e. ( ( rank ` C ) u. ( rank ` D ) ) )
9 rankon 
 |-  ( rank ` C ) e. On
10 rankon 
 |-  ( rank ` D ) e. On
11 9 10 onun2i 
 |-  ( ( rank ` C ) u. ( rank ` D ) ) e. On
12 11 onordi 
 |-  Ord ( ( rank ` C ) u. ( rank ` D ) )
13 ordsucelsuc 
 |-  ( Ord ( ( rank ` C ) u. ( rank ` D ) ) -> ( ( ( rank ` A ) u. ( rank ` B ) ) e. ( ( rank ` C ) u. ( rank ` D ) ) <-> suc ( ( rank ` A ) u. ( rank ` B ) ) e. suc ( ( rank ` C ) u. ( rank ` D ) ) ) )
14 12 13 ax-mp 
 |-  ( ( ( rank ` A ) u. ( rank ` B ) ) e. ( ( rank ` C ) u. ( rank ` D ) ) <-> suc ( ( rank ` A ) u. ( rank ` B ) ) e. suc ( ( rank ` C ) u. ( rank ` D ) ) )
15 8 14 sylib 
 |-  ( ( ( rank ` A ) e. ( rank ` C ) /\ ( rank ` B ) e. ( rank ` D ) ) -> suc ( ( rank ` A ) u. ( rank ` B ) ) e. suc ( ( rank ` C ) u. ( rank ` D ) ) )
16 1 2 rankpr 
 |-  ( rank ` { A , B } ) = suc ( ( rank ` A ) u. ( rank ` B ) )
17 3 4 rankpr 
 |-  ( rank ` { C , D } ) = suc ( ( rank ` C ) u. ( rank ` D ) )
18 15 16 17 3eltr4g 
 |-  ( ( ( rank ` A ) e. ( rank ` C ) /\ ( rank ` B ) e. ( rank ` D ) ) -> ( rank ` { A , B } ) e. ( rank ` { C , D } ) )