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