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