Theorem rankelpr

Description: Rank membership is inherited by unordered pairs. (Contributed by NM, 18-Sep-2006) (Revised 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	rankelpr	|- ( ( ( rank ` A ) e. ( rank ` C ) /\ ( rank ` B ) e. ( rank ` D ) ) -> ( rank ` { A , B } ) e. ( rank ` { C , 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	1 2 3 4	rankelun	|- ( ( ( rank ` A ) e. ( rank ` C ) /\ ( rank ` B ) e. ( rank ` D ) ) -> ( rank ` ( A u. B ) ) e. ( rank ` ( C u. D ) ) )
6	1 2	rankun	|- ( rank ` ( A u. B ) ) = ( ( rank ` A ) u. ( rank ` B ) )
7	3 4	rankun	|- ( rank ` ( C u. D ) ) = ( ( rank ` C ) u. ( rank ` D ) )
8	5 6 7	3eltr3g	|- ( ( ( rank ` A ) e. ( rank ` C ) /\ ( rank ` B ) e. ( rank ` D ) ) -> ( ( rank ` A ) u. ( rank ` B ) ) e. ( ( rank ` C ) u. ( rank ` D ) ) )
9		rankon	|- ( rank ` C ) e. On
10		rankon	|- ( rank ` D ) e. On
11	9 10	onun2i	|- ( ( rank ` C ) u. ( rank ` D ) ) e. On
12	11	onordi	|- Ord ( ( rank ` C ) u. ( rank ` D ) )
13		ordsucelsuc	|- ( Ord ( ( rank ` C ) u. ( rank ` D ) ) -> ( ( ( rank ` A ) u. ( rank ` B ) ) e. ( ( rank ` C ) u. ( rank ` D ) ) <-> suc ( ( rank ` A ) u. ( rank ` B ) ) e. suc ( ( rank ` C ) u. ( rank ` D ) ) ) )
14	12 13	ax-mp	|- ( ( ( rank ` A ) u. ( rank ` B ) ) e. ( ( rank ` C ) u. ( rank ` D ) ) <-> suc ( ( rank ` A ) u. ( rank ` B ) ) e. suc ( ( rank ` C ) u. ( rank ` D ) ) )
15	8 14	sylib	|- ( ( ( rank ` A ) e. ( rank ` C ) /\ ( rank ` B ) e. ( rank ` D ) ) -> suc ( ( rank ` A ) u. ( rank ` B ) ) e. suc ( ( rank ` C ) u. ( rank ` D ) ) )
16	1 2	rankpr	|- ( rank ` { A , B } ) = suc ( ( rank ` A ) u. ( rank ` B ) )
17	3 4	rankpr	|- ( rank ` { C , D } ) = suc ( ( rank ` C ) u. ( rank ` D ) )
18	15 16 17	3eltr4g	|- ( ( ( rank ` A ) e. ( rank ` C ) /\ ( rank ` B ) e. ( rank ` D ) ) -> ( rank ` { A , B } ) e. ( rank ` { C , D } ) )