Theorem rankc2

Description: A relationship that can be used for computation of rank. (Contributed by NM, 16-Sep-2006)

	Ref	Expression
Hypothesis	rankr1b.1	|- A e. _V
Assertion	rankc2	|- ( E. x e. A ( rank ` x ) = ( rank ` U. A ) -> ( rank ` A ) = suc ( rank ` U. A ) )

Proof

Step	Hyp	Ref	Expression
1		rankr1b.1	|- A e. _V
2		pwuni	|- A C_ ~P U. A
3	1	uniex	|- U. A e. _V
4	3	pwex	|- ~P U. A e. _V
5	4	rankss	|- ( A C_ ~P U. A -> ( rank ` A ) C_ ( rank ` ~P U. A ) )
6	2 5	ax-mp	|- ( rank ` A ) C_ ( rank ` ~P U. A )
7	3	rankpw	|- ( rank ` ~P U. A ) = suc ( rank ` U. A )
8	6 7	sseqtri	|- ( rank ` A ) C_ suc ( rank ` U. A )
9	8	a1i	|- ( E. x e. A ( rank ` x ) = ( rank ` U. A ) -> ( rank ` A ) C_ suc ( rank ` U. A ) )
10	1	rankel	|- ( x e. A -> ( rank ` x ) e. ( rank ` A ) )
11		eleq1	|- ( ( rank ` x ) = ( rank ` U. A ) -> ( ( rank ` x ) e. ( rank ` A ) <-> ( rank ` U. A ) e. ( rank ` A ) ) )
12	10 11	syl5ibcom	|- ( x e. A -> ( ( rank ` x ) = ( rank ` U. A ) -> ( rank ` U. A ) e. ( rank ` A ) ) )
13	12	rexlimiv	|- ( E. x e. A ( rank ` x ) = ( rank ` U. A ) -> ( rank ` U. A ) e. ( rank ` A ) )
14		rankon	|- ( rank ` U. A ) e. On
15		rankon	|- ( rank ` A ) e. On
16	14 15	onsucssi	|- ( ( rank ` U. A ) e. ( rank ` A ) <-> suc ( rank ` U. A ) C_ ( rank ` A ) )
17	13 16	sylib	|- ( E. x e. A ( rank ` x ) = ( rank ` U. A ) -> suc ( rank ` U. A ) C_ ( rank ` A ) )
18	9 17	eqssd	|- ( E. x e. A ( rank ` x ) = ( rank ` U. A ) -> ( rank ` A ) = suc ( rank ` U. A ) )