Theorem onuninsuci

Description: A limit ordinal is not a successor ordinal. (Contributed by NM, 18-Feb-2004)

	Ref	Expression
Hypothesis	onssi.1	$$⊢A\in \mathrm{On}$$
Assertion	onuninsuci	$$⊢A=\bigcup A\leftrightarrow \neg \exists x\in \mathrm{On}A=\mathrm{suc}x$$

Proof

Step	Hyp	Ref	Expression
1		onssi.1	$$⊢A\in \mathrm{On}$$
2	1	onirri	$$⊢\neg A\in A$$
3		id	$$⊢A=\bigcup A\to A=\bigcup A$$
4		df-suc	$$⊢\mathrm{suc}x=x\cup \left\{x\right\}$$
5	4	eqeq2i	$$⊢A=\mathrm{suc}x\leftrightarrow A=x\cup \left\{x\right\}$$
6		unieq	$$⊢A=x\cup \left\{x\right\}\to \bigcup A=\bigcup \left(x\cup \left\{x\right\}\right)$$
7	5 6	sylbi	$$⊢A=\mathrm{suc}x\to \bigcup A=\bigcup \left(x\cup \left\{x\right\}\right)$$
8		uniun	$$⊢\bigcup \left(x\cup \left\{x\right\}\right)=\bigcup x\cup \bigcup \left\{x\right\}$$
9		vex	$$⊢x\in \mathrm{V}$$
10	9	unisn	$$⊢\bigcup \left\{x\right\}=x$$
11	10	uneq2i	$$⊢\bigcup x\cup \bigcup \left\{x\right\}=\bigcup x\cup x$$
12	8 11	eqtri	$$⊢\bigcup \left(x\cup \left\{x\right\}\right)=\bigcup x\cup x$$
13	7 12	eqtrdi	$$⊢A=\mathrm{suc}x\to \bigcup A=\bigcup x\cup x$$
14		tron	$$⊢\mathrm{Tr}\mathrm{On}$$
15		eleq1	$$⊢A=\mathrm{suc}x\to \left(A\in \mathrm{On}\leftrightarrow \mathrm{suc}x\in \mathrm{On}\right)$$
16	1 15	mpbii	$$⊢A=\mathrm{suc}x\to \mathrm{suc}x\in \mathrm{On}$$
17		trsuc	$$⊢\left(\mathrm{Tr}\mathrm{On}\wedge \mathrm{suc}x\in \mathrm{On}\right)\to x\in \mathrm{On}$$
18	14 16 17	sylancr	$$⊢A=\mathrm{suc}x\to x\in \mathrm{On}$$
19		eloni	$$⊢x\in \mathrm{On}\to \mathrm{Ord}x$$
20		ordtr	$$⊢\mathrm{Ord}x\to \mathrm{Tr}x$$
21	19 20	syl	$$⊢x\in \mathrm{On}\to \mathrm{Tr}x$$
22		df-tr	$$⊢\mathrm{Tr}x\leftrightarrow \bigcup x\subseteq x$$
23	21 22	sylib	$$⊢x\in \mathrm{On}\to \bigcup x\subseteq x$$
24	18 23	syl	$$⊢A=\mathrm{suc}x\to \bigcup x\subseteq x$$
25		ssequn1	$$⊢\bigcup x\subseteq x\leftrightarrow \bigcup x\cup x=x$$
26	24 25	sylib	$$⊢A=\mathrm{suc}x\to \bigcup x\cup x=x$$
27	13 26	eqtrd	$$⊢A=\mathrm{suc}x\to \bigcup A=x$$
28	3 27	sylan9eqr	$$⊢\left(A=\mathrm{suc}x\wedge A=\bigcup A\right)\to A=x$$
29	9	sucid	$$⊢x\in \mathrm{suc}x$$
30		eleq2	$$⊢A=\mathrm{suc}x\to \left(x\in A\leftrightarrow x\in \mathrm{suc}x\right)$$
31	29 30	mpbiri	$$⊢A=\mathrm{suc}x\to x\in A$$
32	31	adantr	$$⊢\left(A=\mathrm{suc}x\wedge A=\bigcup A\right)\to x\in A$$
33	28 32	eqeltrd	$$⊢\left(A=\mathrm{suc}x\wedge A=\bigcup A\right)\to A\in A$$
34	2 33	mto	$$⊢\neg \left(A=\mathrm{suc}x\wedge A=\bigcup A\right)$$
35	34	imnani	$$⊢A=\mathrm{suc}x\to \neg A=\bigcup A$$
36	35	rexlimivw	$$⊢\exists x\in \mathrm{On}A=\mathrm{suc}x\to \neg A=\bigcup A$$
37		onuni	$$⊢A\in \mathrm{On}\to \bigcup A\in \mathrm{On}$$
38	1 37	ax-mp	$$⊢\bigcup A\in \mathrm{On}$$
39	1	onuniorsuci	$$⊢\left(A=\bigcup A\vee A=\mathrm{suc}\bigcup A\right)$$
40	39	ori	$$⊢\neg A=\bigcup A\to A=\mathrm{suc}\bigcup A$$
41		suceq	$$⊢x=\bigcup A\to \mathrm{suc}x=\mathrm{suc}\bigcup A$$
42	41	rspceeqv	$$⊢\left(\bigcup A\in \mathrm{On}\wedge A=\mathrm{suc}\bigcup A\right)\to \exists x\in \mathrm{On}A=\mathrm{suc}x$$
43	38 40 42	sylancr	$$⊢\neg A=\bigcup A\to \exists x\in \mathrm{On}A=\mathrm{suc}x$$
44	36 43	impbii	$$⊢\exists x\in \mathrm{On}A=\mathrm{suc}x\leftrightarrow \neg A=\bigcup A$$
45	44	con2bii	$$⊢A=\bigcup A\leftrightarrow \neg \exists x\in \mathrm{On}A=\mathrm{suc}x$$