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

Metamath Proof Explorer

Theorem rankssb

Description: The subset relation is inherited by the rank function. Exercise 1 of TakeutiZaring p. 80. (Contributed by NM, 25-Nov-2003) (Revised by Mario Carneiro, 17-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( B e. U. ( R1 " On ) /\ A C_ B ) -> A C_ B )
2 r1rankidb 
 |-  ( B e. U. ( R1 " On ) -> B C_ ( R1 ` ( rank ` B ) ) )
3 2 adantr 
 |-  ( ( B e. U. ( R1 " On ) /\ A C_ B ) -> B C_ ( R1 ` ( rank ` B ) ) )
4 1 3 sstrd 
 |-  ( ( B e. U. ( R1 " On ) /\ A C_ B ) -> A C_ ( R1 ` ( rank ` B ) ) )
5 sswf 
 |-  ( ( B e. U. ( R1 " On ) /\ A C_ B ) -> A e. U. ( R1 " On ) )
6 rankdmr1 
 |-  ( rank ` B ) e. dom R1
7 rankr1bg 
 |-  ( ( A e. U. ( R1 " On ) /\ ( rank ` B ) e. dom R1 ) -> ( A C_ ( R1 ` ( rank ` B ) ) <-> ( rank ` A ) C_ ( rank ` B ) ) )
8 5 6 7 sylancl 
 |-  ( ( B e. U. ( R1 " On ) /\ A C_ B ) -> ( A C_ ( R1 ` ( rank ` B ) ) <-> ( rank ` A ) C_ ( rank ` B ) ) )
9 4 8 mpbid 
 |-  ( ( B e. U. ( R1 " On ) /\ A C_ B ) -> ( rank ` A ) C_ ( rank ` B ) )
10 9 ex 
 |-  ( B e. U. ( R1 " On ) -> ( A C_ B -> ( rank ` A ) C_ ( rank ` B ) ) )