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

Metamath Proof Explorer

Theorem unbnn2

Description: Version of unbnn that does not require a strict upper bound. (Contributed by NM, 24-Apr-2004)

Ref Expression
Assertion unbnn2 
|- ( ( _om e. _V /\ A C_ _om /\ A. x e. _om E. y e. A x C_ y ) -> A ~~ _om )

Proof

Step Hyp Ref Expression
1 peano2 
 |-  ( z e. _om -> suc z e. _om )
2 sseq1 
 |-  ( x = suc z -> ( x C_ y <-> suc z C_ y ) )
3 2 rexbidv 
 |-  ( x = suc z -> ( E. y e. A x C_ y <-> E. y e. A suc z C_ y ) )
4 3 rspcv 
 |-  ( suc z e. _om -> ( A. x e. _om E. y e. A x C_ y -> E. y e. A suc z C_ y ) )
5 sucssel 
 |-  ( z e. _V -> ( suc z C_ y -> z e. y ) )
6 5 elv 
 |-  ( suc z C_ y -> z e. y )
7 6 reximi 
 |-  ( E. y e. A suc z C_ y -> E. y e. A z e. y )
8 4 7 syl6com 
 |-  ( A. x e. _om E. y e. A x C_ y -> ( suc z e. _om -> E. y e. A z e. y ) )
9 1 8 syl5 
 |-  ( A. x e. _om E. y e. A x C_ y -> ( z e. _om -> E. y e. A z e. y ) )
10 9 ralrimiv 
 |-  ( A. x e. _om E. y e. A x C_ y -> A. z e. _om E. y e. A z e. y )
11 unbnn 
 |-  ( ( _om e. _V /\ A C_ _om /\ A. z e. _om E. y e. A z e. y ) -> A ~~ _om )
12 10 11 syl3an3 
 |-  ( ( _om e. _V /\ A C_ _om /\ A. x e. _om E. y e. A x C_ y ) -> A ~~ _om )