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

Metamath Proof Explorer

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