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

Metamath Proof Explorer

Theorem rankelb

Description: The membership relation is inherited by the rank function. Proposition 9.16 of TakeutiZaring p. 79. (Contributed by NM, 4-Oct-2003) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion rankelb 
|- ( B e. U. ( R1 " On ) -> ( A e. B -> ( rank ` A ) e. ( rank ` B ) ) )

Proof

Step Hyp Ref Expression
1 r1elssi 
 |-  ( B e. U. ( R1 " On ) -> B C_ U. ( R1 " On ) )
2 1 sseld 
 |-  ( B e. U. ( R1 " On ) -> ( A e. B -> A e. U. ( R1 " On ) ) )
3 rankidn 
 |-  ( A e. U. ( R1 " On ) -> -. A e. ( R1 ` ( rank ` A ) ) )
4 2 3 syl6 
 |-  ( B e. U. ( R1 " On ) -> ( A e. B -> -. A e. ( R1 ` ( rank ` A ) ) ) )
5 4 imp 
 |-  ( ( B e. U. ( R1 " On ) /\ A e. B ) -> -. A e. ( R1 ` ( rank ` A ) ) )
6 rankon 
 |-  ( rank ` B ) e. On
7 rankon 
 |-  ( rank ` A ) e. On
8 ontri1 
 |-  ( ( ( rank ` B ) e. On /\ ( rank ` A ) e. On ) -> ( ( rank ` B ) C_ ( rank ` A ) <-> -. ( rank ` A ) e. ( rank ` B ) ) )
9 6 7 8 mp2an 
 |-  ( ( rank ` B ) C_ ( rank ` A ) <-> -. ( rank ` A ) e. ( rank ` B ) )
10 rankdmr1 
 |-  ( rank ` B ) e. dom R1
11 rankdmr1 
 |-  ( rank ` A ) e. dom R1
12 r1ord3g 
 |-  ( ( ( rank ` B ) e. dom R1 /\ ( rank ` A ) e. dom R1 ) -> ( ( rank ` B ) C_ ( rank ` A ) -> ( R1 ` ( rank ` B ) ) C_ ( R1 ` ( rank ` A ) ) ) )
13 10 11 12 mp2an 
 |-  ( ( rank ` B ) C_ ( rank ` A ) -> ( R1 ` ( rank ` B ) ) C_ ( R1 ` ( rank ` A ) ) )
14 r1rankidb 
 |-  ( B e. U. ( R1 " On ) -> B C_ ( R1 ` ( rank ` B ) ) )
15 14 sselda 
 |-  ( ( B e. U. ( R1 " On ) /\ A e. B ) -> A e. ( R1 ` ( rank ` B ) ) )
16 ssel 
 |-  ( ( R1 ` ( rank ` B ) ) C_ ( R1 ` ( rank ` A ) ) -> ( A e. ( R1 ` ( rank ` B ) ) -> A e. ( R1 ` ( rank ` A ) ) ) )
17 13 15 16 syl2imc 
 |-  ( ( B e. U. ( R1 " On ) /\ A e. B ) -> ( ( rank ` B ) C_ ( rank ` A ) -> A e. ( R1 ` ( rank ` A ) ) ) )
18 9 17 biimtrrid 
 |-  ( ( B e. U. ( R1 " On ) /\ A e. B ) -> ( -. ( rank ` A ) e. ( rank ` B ) -> A e. ( R1 ` ( rank ` A ) ) ) )
19 5 18 mt3d 
 |-  ( ( B e. U. ( R1 " On ) /\ A e. B ) -> ( rank ` A ) e. ( rank ` B ) )
20 19 ex 
 |-  ( B e. U. ( R1 " On ) -> ( A e. B -> ( rank ` A ) e. ( rank ` B ) ) )