This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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