Metamath Proof Explorer


Theorem onuninsuci

Description: An ordinal is equal to its union if and only if it is not the successor of an ordinal. A closed-form generalization of this result is orduninsuc . (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 unisnv
 |-  U. { x } = x
10 9 uneq2i
 |-  ( U. x u. U. { x } ) = ( U. x u. x )
11 8 10 eqtri
 |-  U. ( x u. { x } ) = ( U. x u. x )
12 7 11 eqtrdi
 |-  ( A = suc x -> U. A = ( U. x u. x ) )
13 tron
 |-  Tr On
14 eleq1
 |-  ( A = suc x -> ( A e. On <-> suc x e. On ) )
15 1 14 mpbii
 |-  ( A = suc x -> suc x e. On )
16 trsuc
 |-  ( ( Tr On /\ suc x e. On ) -> x e. On )
17 13 15 16 sylancr
 |-  ( A = suc x -> x e. On )
18 ontr
 |-  ( x e. On -> Tr x )
19 df-tr
 |-  ( Tr x <-> U. x C_ x )
20 18 19 sylib
 |-  ( x e. On -> U. x C_ x )
21 17 20 syl
 |-  ( A = suc x -> U. x C_ x )
22 ssequn1
 |-  ( U. x C_ x <-> ( U. x u. x ) = x )
23 21 22 sylib
 |-  ( A = suc x -> ( U. x u. x ) = x )
24 12 23 eqtrd
 |-  ( A = suc x -> U. A = x )
25 3 24 sylan9eqr
 |-  ( ( A = suc x /\ A = U. A ) -> A = x )
26 vex
 |-  x e. _V
27 26 sucid
 |-  x e. suc x
28 eleq2
 |-  ( A = suc x -> ( x e. A <-> x e. suc x ) )
29 27 28 mpbiri
 |-  ( A = suc x -> x e. A )
30 29 adantr
 |-  ( ( A = suc x /\ A = U. A ) -> x e. A )
31 25 30 eqeltrd
 |-  ( ( A = suc x /\ A = U. A ) -> A e. A )
32 2 31 mto
 |-  -. ( A = suc x /\ A = U. A )
33 32 imnani
 |-  ( A = suc x -> -. A = U. A )
34 33 rexlimivw
 |-  ( E. x e. On A = suc x -> -. A = U. A )
35 onuni
 |-  ( A e. On -> U. A e. On )
36 1 35 ax-mp
 |-  U. A e. On
37 onuniorsuc
 |-  ( A e. On -> ( A = U. A \/ A = suc U. A ) )
38 1 37 ax-mp
 |-  ( A = U. A \/ A = suc U. A )
39 38 ori
 |-  ( -. A = U. A -> A = suc U. A )
40 suceq
 |-  ( x = U. A -> suc x = suc U. A )
41 40 rspceeqv
 |-  ( ( U. A e. On /\ A = suc U. A ) -> E. x e. On A = suc x )
42 36 39 41 sylancr
 |-  ( -. A = U. A -> E. x e. On A = suc x )
43 34 42 impbii
 |-  ( E. x e. On A = suc x <-> -. A = U. A )
44 43 con2bii
 |-  ( A = U. A <-> -. E. x e. On A = suc x )