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 ) )