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