Theorem ssorduni

Description: The union of a class of ordinal numbers is ordinal. Proposition 7.19 of TakeutiZaring p. 40. (Contributed by NM, 30-May-1994) (Proof shortened by Andrew Salmon, 12-Aug-2011)

	Ref	Expression
Assertion	ssorduni	|- ( A C_ On -> Ord U. A )

Proof

Step	Hyp	Ref	Expression
1		eluni2	|- ( x e. U. A <-> E. y e. A x e. y )
2		ssel	|- ( A C_ On -> ( y e. A -> y e. On ) )
3		onelss	|- ( y e. On -> ( x e. y -> x C_ y ) )
4	2 3	syl6	|- ( A C_ On -> ( y e. A -> ( x e. y -> x C_ y ) ) )
5		anc2r	|- ( ( y e. A -> ( x e. y -> x C_ y ) ) -> ( y e. A -> ( x e. y -> ( x C_ y /\ y e. A ) ) ) )
6	4 5	syl	|- ( A C_ On -> ( y e. A -> ( x e. y -> ( x C_ y /\ y e. A ) ) ) )
7		ssuni	|- ( ( x C_ y /\ y e. A ) -> x C_ U. A )
8	6 7	syl8	|- ( A C_ On -> ( y e. A -> ( x e. y -> x C_ U. A ) ) )
9	8	rexlimdv	|- ( A C_ On -> ( E. y e. A x e. y -> x C_ U. A ) )
10	1 9	syl5bi	|- ( A C_ On -> ( x e. U. A -> x C_ U. A ) )
11	10	ralrimiv	|- ( A C_ On -> A. x e. U. A x C_ U. A )
12		dftr3	|- ( Tr U. A <-> A. x e. U. A x C_ U. A )
13	11 12	sylibr	|- ( A C_ On -> Tr U. A )
14		onelon	|- ( ( y e. On /\ x e. y ) -> x e. On )
15	14	ex	|- ( y e. On -> ( x e. y -> x e. On ) )
16	2 15	syl6	|- ( A C_ On -> ( y e. A -> ( x e. y -> x e. On ) ) )
17	16	rexlimdv	|- ( A C_ On -> ( E. y e. A x e. y -> x e. On ) )
18	1 17	syl5bi	|- ( A C_ On -> ( x e. U. A -> x e. On ) )
19	18	ssrdv	|- ( A C_ On -> U. A C_ On )
20		ordon	|- Ord On
21		trssord	|- ( ( Tr U. A /\ U. A C_ On /\ Ord On ) -> Ord U. A )
22	21	3exp	|- ( Tr U. A -> ( U. A C_ On -> ( Ord On -> Ord U. A ) ) )
23	20 22	mpii	|- ( Tr U. A -> ( U. A C_ On -> Ord U. A ) )
24	13 19 23	sylc	|- ( A C_ On -> Ord U. A )