Theorem onuninsuci

Description: An ordinal is equal to its union if and only if it is not the successor of an ordinal. A closed-form generalization of this result is orduninsuc . (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		unisnv	$$⊢\bigcup \left\{x\right\}=x$$
10	9	uneq2i	$$⊢\bigcup x\cup \bigcup \left\{x\right\}=\bigcup x\cup x$$
11	8 10	eqtri	$$⊢\bigcup \left(x\cup \left\{x\right\}\right)=\bigcup x\cup x$$
12	7 11	eqtrdi	$$⊢A=\mathrm{suc}x\to \bigcup A=\bigcup x\cup x$$
13		tron	$$⊢\mathrm{Tr}\mathrm{On}$$
14		eleq1	$$⊢A=\mathrm{suc}x\to \left(A\in \mathrm{On}\leftrightarrow \mathrm{suc}x\in \mathrm{On}\right)$$
15	1 14	mpbii	$$⊢A=\mathrm{suc}x\to \mathrm{suc}x\in \mathrm{On}$$
16		trsuc	$$⊢\left(\mathrm{Tr}\mathrm{On}\wedge \mathrm{suc}x\in \mathrm{On}\right)\to x\in \mathrm{On}$$
17	13 15 16	sylancr	$$⊢A=\mathrm{suc}x\to x\in \mathrm{On}$$
18		ontr	$$⊢x\in \mathrm{On}\to \mathrm{Tr}x$$
19		df-tr	$$⊢\mathrm{Tr}x\leftrightarrow \bigcup x\subseteq x$$
20	18 19	sylib	$$⊢x\in \mathrm{On}\to \bigcup x\subseteq x$$
21	17 20	syl	$$⊢A=\mathrm{suc}x\to \bigcup x\subseteq x$$
22		ssequn1	$$⊢\bigcup x\subseteq x\leftrightarrow \bigcup x\cup x=x$$
23	21 22	sylib	$$⊢A=\mathrm{suc}x\to \bigcup x\cup x=x$$
24	12 23	eqtrd	$$⊢A=\mathrm{suc}x\to \bigcup A=x$$
25	3 24	sylan9eqr	$$⊢\left(A=\mathrm{suc}x\wedge A=\bigcup A\right)\to A=x$$
26		vex	$$⊢x\in \mathrm{V}$$
27	26	sucid	$$⊢x\in \mathrm{suc}x$$
28		eleq2	$$⊢A=\mathrm{suc}x\to \left(x\in A\leftrightarrow x\in \mathrm{suc}x\right)$$
29	27 28	mpbiri	$$⊢A=\mathrm{suc}x\to x\in A$$
30	29	adantr	$$⊢\left(A=\mathrm{suc}x\wedge A=\bigcup A\right)\to x\in A$$
31	25 30	eqeltrd	$$⊢\left(A=\mathrm{suc}x\wedge A=\bigcup A\right)\to A\in A$$
32	2 31	mto	$$⊢\neg \left(A=\mathrm{suc}x\wedge A=\bigcup A\right)$$
33	32	imnani	$$⊢A=\mathrm{suc}x\to \neg A=\bigcup A$$
34	33	rexlimivw	$$⊢\exists x\in \mathrm{On}A=\mathrm{suc}x\to \neg A=\bigcup A$$
35		onuni	$$⊢A\in \mathrm{On}\to \bigcup A\in \mathrm{On}$$
36	1 35	ax-mp	$$⊢\bigcup A\in \mathrm{On}$$
37		onuniorsuc	$$⊢A\in \mathrm{On}\to \left(A=\bigcup A\vee A=\mathrm{suc}\bigcup A\right)$$
38	1 37	ax-mp	$$⊢\left(A=\bigcup A\vee A=\mathrm{suc}\bigcup A\right)$$
39	38	ori	$$⊢\neg A=\bigcup A\to A=\mathrm{suc}\bigcup A$$
40		suceq	$$⊢x=\bigcup A\to \mathrm{suc}x=\mathrm{suc}\bigcup A$$
41	40	rspceeqv	$$⊢\left(\bigcup A\in \mathrm{On}\wedge A=\mathrm{suc}\bigcup A\right)\to \exists x\in \mathrm{On}A=\mathrm{suc}x$$
42	36 39 41	sylancr	$$⊢\neg A=\bigcup A\to \exists x\in \mathrm{On}A=\mathrm{suc}x$$
43	34 42	impbii	$$⊢\exists x\in \mathrm{On}A=\mathrm{suc}x\leftrightarrow \neg A=\bigcup A$$
44	43	con2bii	$$⊢A=\bigcup A\leftrightarrow \neg \exists x\in \mathrm{On}A=\mathrm{suc}x$$