Metamath Proof Explorer

Theorem rankelun

Description: Rank membership is inherited by union. (Contributed by NM, 18-Sep-2006) (Proof shortened 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 rankelun 
|- ( ( ( rank ` A ) e. ( rank ` C ) /\ ( rank ` B ) e. ( rank ` D ) ) -> ( rank ` ( A u. B ) ) e. ( rank ` ( C u. 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 rankon 
 |-  ( rank ` C ) e. On
6 rankon 
 |-  ( rank ` D ) e. On
7 5 6 onun2i 
 |-  ( ( rank ` C ) u. ( rank ` D ) ) e. On
8 7 onordi 
 |-  Ord ( ( rank ` C ) u. ( rank ` D ) )
9 elun1 
 |-  ( ( rank ` A ) e. ( rank ` C ) -> ( rank ` A ) e. ( ( rank ` C ) u. ( rank ` D ) ) )
10 elun2 
 |-  ( ( rank ` B ) e. ( rank ` D ) -> ( rank ` B ) e. ( ( rank ` C ) u. ( rank ` D ) ) )
11 ordunel 
 |-  ( ( Ord ( ( rank ` C ) u. ( rank ` D ) ) /\ ( rank ` A ) e. ( ( rank ` C ) u. ( rank ` D ) ) /\ ( rank ` B ) e. ( ( rank ` C ) u. ( rank ` D ) ) ) -> ( ( rank ` A ) u. ( rank ` B ) ) e. ( ( rank ` C ) u. ( rank ` D ) ) )
12 8 9 10 11 mp3an3an 
 |-  ( ( ( rank ` A ) e. ( rank ` C ) /\ ( rank ` B ) e. ( rank ` D ) ) -> ( ( rank ` A ) u. ( rank ` B ) ) e. ( ( rank ` C ) u. ( rank ` D ) ) )
13 1 2 rankun 
 |-  ( rank ` ( A u. B ) ) = ( ( rank ` A ) u. ( rank ` B ) )
14 3 4 rankun 
 |-  ( rank ` ( C u. D ) ) = ( ( rank ` C ) u. ( rank ` D ) )
15 12 13 14 3eltr4g 
 |-  ( ( ( rank ` A ) e. ( rank ` C ) /\ ( rank ` B ) e. ( rank ` D ) ) -> ( rank ` ( A u. B ) ) e. ( rank ` ( C u. D ) ) )