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

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 )