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 )