Metamath Proof Explorer

Theorem onuninsuci

Description: A limit ordinal is not a successor ordinal. (Contributed by NM, 18-Feb-2004)

Ref Expression
Hypothesis onssi.1 
|- A e. On
Assertion onuninsuci 
|- ( A = U. A <-> -. E. x e. On A = suc x )

Proof

Step Hyp Ref Expression
1 onssi.1 
 |-  A e. On
2 1 onirri 
 |-  -. A e. A
3 id 
 |-  ( A = U. A -> A = U. A )
4 df-suc 
 |-  suc x = ( x u. { x } )
5 4 eqeq2i 
 |-  ( A = suc x <-> A = ( x u. { x } ) )
6 unieq 
 |-  ( A = ( x u. { x } ) -> U. A = U. ( x u. { x } ) )
7 5 6 sylbi 
 |-  ( A = suc x -> U. A = U. ( x u. { x } ) )
8 uniun 
 |-  U. ( x u. { x } ) = ( U. x u. U. { x } )
9 vex 
 |-  x e. _V
10 9 unisn 
 |-  U. { x } = x
11 10 uneq2i 
 |-  ( U. x u. U. { x } ) = ( U. x u. x )
12 8 11 eqtri 
 |-  U. ( x u. { x } ) = ( U. x u. x )
13 7 12 eqtrdi 
 |-  ( A = suc x -> U. A = ( U. x u. x ) )
14 tron 
 |-  Tr On
15 eleq1 
 |-  ( A = suc x -> ( A e. On <-> suc x e. On ) )
16 1 15 mpbii 
 |-  ( A = suc x -> suc x e. On )
17 trsuc 
 |-  ( ( Tr On /\ suc x e. On ) -> x e. On )
18 14 16 17 sylancr 
 |-  ( A = suc x -> x e. On )
19 eloni 
 |-  ( x e. On -> Ord x )
20 ordtr 
 |-  ( Ord x -> Tr x )
21 19 20 syl 
 |-  ( x e. On -> Tr x )
22 df-tr 
 |-  ( Tr x <-> U. x C_ x )
23 21 22 sylib 
 |-  ( x e. On -> U. x C_ x )
24 18 23 syl 
 |-  ( A = suc x -> U. x C_ x )
25 ssequn1 
 |-  ( U. x C_ x <-> ( U. x u. x ) = x )
26 24 25 sylib 
 |-  ( A = suc x -> ( U. x u. x ) = x )
27 13 26 eqtrd 
 |-  ( A = suc x -> U. A = x )
28 3 27 sylan9eqr 
 |-  ( ( A = suc x /\ A = U. A ) -> A = x )
29 9 sucid 
 |-  x e. suc x
30 eleq2 
 |-  ( A = suc x -> ( x e. A <-> x e. suc x ) )
31 29 30 mpbiri 
 |-  ( A = suc x -> x e. A )
32 31 adantr 
 |-  ( ( A = suc x /\ A = U. A ) -> x e. A )
33 28 32 eqeltrd 
 |-  ( ( A = suc x /\ A = U. A ) -> A e. A )
34 2 33 mto 
 |-  -. ( A = suc x /\ A = U. A )
35 34 imnani 
 |-  ( A = suc x -> -. A = U. A )
36 35 rexlimivw 
 |-  ( E. x e. On A = suc x -> -. A = U. A )
37 onuni 
 |-  ( A e. On -> U. A e. On )
38 1 37 ax-mp 
 |-  U. A e. On
39 1 onuniorsuci 
 |-  ( A = U. A \/ A = suc U. A )
40 39 ori 
 |-  ( -. A = U. A -> A = suc U. A )
41 suceq 
 |-  ( x = U. A -> suc x = suc U. A )
42 41 rspceeqv 
 |-  ( ( U. A e. On /\ A = suc U. A ) -> E. x e. On A = suc x )
43 38 40 42 sylancr 
 |-  ( -. A = U. A -> E. x e. On A = suc x )
44 36 43 impbii 
 |-  ( E. x e. On A = suc x <-> -. A = U. A )
45 44 con2bii 
 |-  ( A = U. A <-> -. E. x e. On A = suc x )