Theorem ordtoplem

Description: Membership of the class of successor ordinals. (Contributed by Chen-Pang He, 1-Nov-2015)

	Ref	Expression
Hypothesis	ordtoplem.1	$$⊢\bigcup A\in \mathrm{On}\to \mathrm{suc}\bigcup A\in S$$
Assertion	ordtoplem	$$⊢\mathrm{Ord}A\to \left(A\ne \bigcup A\to A\in S\right)$$

Proof

Step	Hyp	Ref	Expression
1		ordtoplem.1	$$⊢\bigcup A\in \mathrm{On}\to \mathrm{suc}\bigcup A\in S$$
2		df-ne	$$⊢A\ne \bigcup A\leftrightarrow \neg A=\bigcup A$$
3		ordeleqon	$$⊢\mathrm{Ord}A\leftrightarrow \left(A\in \mathrm{On}\vee A=\mathrm{On}\right)$$
4		unon	$$⊢\bigcup \mathrm{On}=\mathrm{On}$$
5	4	eqcomi	$$⊢\mathrm{On}=\bigcup \mathrm{On}$$
6		id	$$⊢A=\mathrm{On}\to A=\mathrm{On}$$
7		unieq	$$⊢A=\mathrm{On}\to \bigcup A=\bigcup \mathrm{On}$$
8	5 6 7	3eqtr4a	$$⊢A=\mathrm{On}\to A=\bigcup A$$
9	8	orim2i	$$⊢\left(A\in \mathrm{On}\vee A=\mathrm{On}\right)\to \left(A\in \mathrm{On}\vee A=\bigcup A\right)$$
10	3 9	sylbi	$$⊢\mathrm{Ord}A\to \left(A\in \mathrm{On}\vee A=\bigcup A\right)$$
11	10	orcomd	$$⊢\mathrm{Ord}A\to \left(A=\bigcup A\vee A\in \mathrm{On}\right)$$
12	11	ord	$$⊢\mathrm{Ord}A\to \left(\neg A=\bigcup A\to A\in \mathrm{On}\right)$$
13		orduniorsuc	$$⊢\mathrm{Ord}A\to \left(A=\bigcup A\vee A=\mathrm{suc}\bigcup A\right)$$
14	13	ord	$$⊢\mathrm{Ord}A\to \left(\neg A=\bigcup A\to A=\mathrm{suc}\bigcup A\right)$$
15		onuni	$$⊢A\in \mathrm{On}\to \bigcup A\in \mathrm{On}$$
16		eleq1a	$$⊢\mathrm{suc}\bigcup A\in S\to \left(A=\mathrm{suc}\bigcup A\to A\in S\right)$$
17	15 1 16	3syl	$$⊢A\in \mathrm{On}\to \left(A=\mathrm{suc}\bigcup A\to A\in S\right)$$
18	12 14 17	syl6c	$$⊢\mathrm{Ord}A\to \left(\neg A=\bigcup A\to A\in S\right)$$
19	2 18	syl5bi	$$⊢\mathrm{Ord}A\to \left(A\ne \bigcup A\to A\in S\right)$$