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

Metamath Proof Explorer

Theorem orduninsuc

Description: An ordinal class is equal to its union if and only if it is not the successor of an ordinal. Closed-form generalization of onuninsuci . (Contributed by NM, 18-Feb-2004)

Ref Expression
Assertion orduninsuc 
|- ( Ord A -> ( A = U. A <-> -. E. x e. On A = suc x ) )

Proof

Step Hyp Ref Expression
1 ordeleqon 
 |-  ( Ord A <-> ( A e. On \/ A = On ) )
2 id 
 |-  ( A = if ( A e. On , A , (/) ) -> A = if ( A e. On , A , (/) ) )
3 unieq 
 |-  ( A = if ( A e. On , A , (/) ) -> U. A = U. if ( A e. On , A , (/) ) )
4 2 3 eqeq12d 
 |-  ( A = if ( A e. On , A , (/) ) -> ( A = U. A <-> if ( A e. On , A , (/) ) = U. if ( A e. On , A , (/) ) ) )
5 eqeq1 
 |-  ( A = if ( A e. On , A , (/) ) -> ( A = suc x <-> if ( A e. On , A , (/) ) = suc x ) )
6 5 rexbidv 
 |-  ( A = if ( A e. On , A , (/) ) -> ( E. x e. On A = suc x <-> E. x e. On if ( A e. On , A , (/) ) = suc x ) )
7 6 notbid 
 |-  ( A = if ( A e. On , A , (/) ) -> ( -. E. x e. On A = suc x <-> -. E. x e. On if ( A e. On , A , (/) ) = suc x ) )
8 4 7 bibi12d 
 |-  ( A = if ( A e. On , A , (/) ) -> ( ( A = U. A <-> -. E. x e. On A = suc x ) <-> ( if ( A e. On , A , (/) ) = U. if ( A e. On , A , (/) ) <-> -. E. x e. On if ( A e. On , A , (/) ) = suc x ) ) )
9 0elon 
 |-  (/) e. On
10 9 elimel 
 |-  if ( A e. On , A , (/) ) e. On
11 10 onuninsuci 
 |-  ( if ( A e. On , A , (/) ) = U. if ( A e. On , A , (/) ) <-> -. E. x e. On if ( A e. On , A , (/) ) = suc x )
12 8 11 dedth 
 |-  ( A e. On -> ( A = U. A <-> -. E. x e. On A = suc x ) )
13 unon 
 |-  U. On = On
14 13 eqcomi 
 |-  On = U. On
15 onprc 
 |-  -. On e. _V
16 vex 
 |-  x e. _V
17 16 sucex 
 |-  suc x e. _V
18 eleq1 
 |-  ( On = suc x -> ( On e. _V <-> suc x e. _V ) )
19 17 18 mpbiri 
 |-  ( On = suc x -> On e. _V )
20 15 19 mto 
 |-  -. On = suc x
21 20 a1i 
 |-  ( x e. On -> -. On = suc x )
22 21 nrex 
 |-  -. E. x e. On On = suc x
23 14 22 2th 
 |-  ( On = U. On <-> -. E. x e. On On = suc x )
24 id 
 |-  ( A = On -> A = On )
25 unieq 
 |-  ( A = On -> U. A = U. On )
26 24 25 eqeq12d 
 |-  ( A = On -> ( A = U. A <-> On = U. On ) )
27 eqeq1 
 |-  ( A = On -> ( A = suc x <-> On = suc x ) )
28 27 rexbidv 
 |-  ( A = On -> ( E. x e. On A = suc x <-> E. x e. On On = suc x ) )
29 28 notbid 
 |-  ( A = On -> ( -. E. x e. On A = suc x <-> -. E. x e. On On = suc x ) )
30 26 29 bibi12d 
 |-  ( A = On -> ( ( A = U. A <-> -. E. x e. On A = suc x ) <-> ( On = U. On <-> -. E. x e. On On = suc x ) ) )
31 23 30 mpbiri 
 |-  ( A = On -> ( A = U. A <-> -. E. x e. On A = suc x ) )
32 12 31 jaoi 
 |-  ( ( A e. On \/ A = On ) -> ( A = U. A <-> -. E. x e. On A = suc x ) )
33 1 32 sylbi 
 |-  ( Ord A -> ( A = U. A <-> -. E. x e. On A = suc x ) )