Theorem onsupnmax

Description: If the union of a class of ordinals is not the maximum element of that class, then the union is a limit ordinal or empty. But this isn't a biconditional since A could be a non-empty set where a limit ordinal or the empty set happens to be the largest element. (Contributed by RP, 27-Jan-2025)

	Ref	Expression
Assertion	onsupnmax	$$⊢A\subseteq \mathrm{On}\to \left(\neg \bigcup A\in A\to \bigcup A=\bigcup \bigcup A\right)$$

Proof

Step	Hyp	Ref	Expression
1		rexnal	$$⊢\exists x\in A\neg \exists y\in Ax\in y\leftrightarrow \neg \forall x\in A\exists y\in Ax\in y$$
2		ralnex	$$⊢\forall y\in A\neg x\in y\leftrightarrow \neg \exists y\in Ax\in y$$
3	2	rexbii	$$⊢\exists x\in A\forall y\in A\neg x\in y\leftrightarrow \exists x\in A\neg \exists y\in Ax\in y$$
4		ssunib	$$⊢A\subseteq \bigcup A\leftrightarrow \forall x\in A\exists y\in Ax\in y$$
5	4	notbii	$$⊢\neg A\subseteq \bigcup A\leftrightarrow \neg \forall x\in A\exists y\in Ax\in y$$
6	1 3 5	3bitr4ri	$$⊢\neg A\subseteq \bigcup A\leftrightarrow \exists x\in A\forall y\in A\neg x\in y$$
7		simpll	$$⊢\left(\left(A\subseteq \mathrm{On}\wedge \bigcup A\in \mathrm{On}\right)\wedge x\in A\right)\to A\subseteq \mathrm{On}$$
8	7	sselda	$$⊢\left(\left(\left(A\subseteq \mathrm{On}\wedge \bigcup A\in \mathrm{On}\right)\wedge x\in A\right)\wedge y\in A\right)\to y\in \mathrm{On}$$
9		simpl	$$⊢\left(A\subseteq \mathrm{On}\wedge \bigcup A\in \mathrm{On}\right)\to A\subseteq \mathrm{On}$$
10	9	sselda	$$⊢\left(\left(A\subseteq \mathrm{On}\wedge \bigcup A\in \mathrm{On}\right)\wedge x\in A\right)\to x\in \mathrm{On}$$
11	10	adantr	$$⊢\left(\left(\left(A\subseteq \mathrm{On}\wedge \bigcup A\in \mathrm{On}\right)\wedge x\in A\right)\wedge y\in A\right)\to x\in \mathrm{On}$$
12		ontri1	$$⊢\left(y\in \mathrm{On}\wedge x\in \mathrm{On}\right)\to \left(y\subseteq x\leftrightarrow \neg x\in y\right)$$
13	8 11 12	syl2anc	$$⊢\left(\left(\left(A\subseteq \mathrm{On}\wedge \bigcup A\in \mathrm{On}\right)\wedge x\in A\right)\wedge y\in A\right)\to \left(y\subseteq x\leftrightarrow \neg x\in y\right)$$
14	13	ralbidva	$$⊢\left(\left(A\subseteq \mathrm{On}\wedge \bigcup A\in \mathrm{On}\right)\wedge x\in A\right)\to \left(\forall y\in Ay\subseteq x\leftrightarrow \forall y\in A\neg x\in y\right)$$
15	14	rexbidva	$$⊢\left(A\subseteq \mathrm{On}\wedge \bigcup A\in \mathrm{On}\right)\to \left(\exists x\in A\forall y\in Ay\subseteq x\leftrightarrow \exists x\in A\forall y\in A\neg x\in y\right)$$
16	6 15	bitr4id	$$⊢\left(A\subseteq \mathrm{On}\wedge \bigcup A\in \mathrm{On}\right)\to \left(\neg A\subseteq \bigcup A\leftrightarrow \exists x\in A\forall y\in Ay\subseteq x\right)$$
17		unielid	$$⊢\bigcup A\in A\leftrightarrow \exists x\in A\forall y\in Ay\subseteq x$$
18	17	a1i	$$⊢\left(A\subseteq \mathrm{On}\wedge \bigcup A\in \mathrm{On}\right)\to \left(\bigcup A\in A\leftrightarrow \exists x\in A\forall y\in Ay\subseteq x\right)$$
19	18	biimprd	$$⊢\left(A\subseteq \mathrm{On}\wedge \bigcup A\in \mathrm{On}\right)\to \left(\exists x\in A\forall y\in Ay\subseteq x\to \bigcup A\in A\right)$$
20	16 19	sylbid	$$⊢\left(A\subseteq \mathrm{On}\wedge \bigcup A\in \mathrm{On}\right)\to \left(\neg A\subseteq \bigcup A\to \bigcup A\in A\right)$$
21	20	con1d	$$⊢\left(A\subseteq \mathrm{On}\wedge \bigcup A\in \mathrm{On}\right)\to \left(\neg \bigcup A\in A\to A\subseteq \bigcup A\right)$$
22		uniss	$$⊢A\subseteq \bigcup A\to \bigcup A\subseteq \bigcup \bigcup A$$
23	21 22	syl6	$$⊢\left(A\subseteq \mathrm{On}\wedge \bigcup A\in \mathrm{On}\right)\to \left(\neg \bigcup A\in A\to \bigcup A\subseteq \bigcup \bigcup A\right)$$
24		ssorduni	$$⊢A\subseteq \mathrm{On}\to \mathrm{Ord}\bigcup A$$
25		orduniss	$$⊢\mathrm{Ord}\bigcup A\to \bigcup \bigcup A\subseteq \bigcup A$$
26	24 25	syl	$$⊢A\subseteq \mathrm{On}\to \bigcup \bigcup A\subseteq \bigcup A$$
27	26	biantrud	$$⊢A\subseteq \mathrm{On}\to \left(\bigcup A\subseteq \bigcup \bigcup A\leftrightarrow \left(\bigcup A\subseteq \bigcup \bigcup A\wedge \bigcup \bigcup A\subseteq \bigcup A\right)\right)$$
28		eqss	$$⊢\bigcup A=\bigcup \bigcup A\leftrightarrow \left(\bigcup A\subseteq \bigcup \bigcup A\wedge \bigcup \bigcup A\subseteq \bigcup A\right)$$
29	27 28	bitr4di	$$⊢A\subseteq \mathrm{On}\to \left(\bigcup A\subseteq \bigcup \bigcup A\leftrightarrow \bigcup A=\bigcup \bigcup A\right)$$
30	29	adantr	$$⊢\left(A\subseteq \mathrm{On}\wedge \bigcup A\in \mathrm{On}\right)\to \left(\bigcup A\subseteq \bigcup \bigcup A\leftrightarrow \bigcup A=\bigcup \bigcup A\right)$$
31	23 30	sylibd	$$⊢\left(A\subseteq \mathrm{On}\wedge \bigcup A\in \mathrm{On}\right)\to \left(\neg \bigcup A\in A\to \bigcup A=\bigcup \bigcup A\right)$$
32	31	ex	$$⊢A\subseteq \mathrm{On}\to \left(\bigcup A\in \mathrm{On}\to \left(\neg \bigcup A\in A\to \bigcup A=\bigcup \bigcup A\right)\right)$$
33		unon	$$⊢\bigcup \mathrm{On}=\mathrm{On}$$
34	33	a1i	$$⊢\bigcup A=\mathrm{On}\to \bigcup \mathrm{On}=\mathrm{On}$$
35		unieq	$$⊢\bigcup A=\mathrm{On}\to \bigcup \bigcup A=\bigcup \mathrm{On}$$
36		id	$$⊢\bigcup A=\mathrm{On}\to \bigcup A=\mathrm{On}$$
37	34 35 36	3eqtr4rd	$$⊢\bigcup A=\mathrm{On}\to \bigcup A=\bigcup \bigcup A$$
38	37	a1i13	$$⊢A\subseteq \mathrm{On}\to \left(\bigcup A=\mathrm{On}\to \left(\neg \bigcup A\in A\to \bigcup A=\bigcup \bigcup A\right)\right)$$
39		ordeleqon	$$⊢\mathrm{Ord}\bigcup A\leftrightarrow \left(\bigcup A\in \mathrm{On}\vee \bigcup A=\mathrm{On}\right)$$
40	24 39	sylib	$$⊢A\subseteq \mathrm{On}\to \left(\bigcup A\in \mathrm{On}\vee \bigcup A=\mathrm{On}\right)$$
41	32 38 40	mpjaod	$$⊢A\subseteq \mathrm{On}\to \left(\neg \bigcup A\in A\to \bigcup A=\bigcup \bigcup A\right)$$