Theorem rankc1

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	rankc1	|- ( A. x e. A ( rank ` x ) e. ( rank ` U. A ) <-> ( rank ` A ) = ( rank ` U. A ) )

Proof

Step	Hyp	Ref	Expression
1		rankr1b.1	|- A e. _V
2	1	rankuniss	|- ( rank ` U. A ) C_ ( rank ` A )
3	2	biantru	|- ( ( rank ` A ) C_ ( rank ` U. A ) <-> ( ( rank ` A ) C_ ( rank ` U. A ) /\ ( rank ` U. A ) C_ ( rank ` A ) ) )
4		iunss	|- ( U_ x e. A suc ( rank ` x ) C_ ( rank ` U. A ) <-> A. x e. A suc ( rank ` x ) C_ ( rank ` U. A ) )
5	1	rankval4	|- ( rank ` A ) = U_ x e. A suc ( rank ` x )
6	5	sseq1i	|- ( ( rank ` A ) C_ ( rank ` U. A ) <-> U_ x e. A suc ( rank ` x ) C_ ( rank ` U. A ) )
7		rankon	|- ( rank ` x ) e. On
8		rankon	|- ( rank ` U. A ) e. On
9	7 8	onsucssi	|- ( ( rank ` x ) e. ( rank ` U. A ) <-> suc ( rank ` x ) C_ ( rank ` U. A ) )
10	9	ralbii	|- ( A. x e. A ( rank ` x ) e. ( rank ` U. A ) <-> A. x e. A suc ( rank ` x ) C_ ( rank ` U. A ) )
11	4 6 10	3bitr4ri	|- ( A. x e. A ( rank ` x ) e. ( rank ` U. A ) <-> ( rank ` A ) C_ ( rank ` U. A ) )
12		eqss	|- ( ( rank ` A ) = ( rank ` U. A ) <-> ( ( rank ` A ) C_ ( rank ` U. A ) /\ ( rank ` U. A ) C_ ( rank ` A ) ) )
13	3 11 12	3bitr4i	|- ( A. x e. A ( rank ` x ) e. ( rank ` U. A ) <-> ( rank ` A ) = ( rank ` U. A ) )