Theorem onsupeqnmax

Description: Condition when the supremum of a class of ordinals is not the maximum element of that class. (Contributed by RP, 27-Jan-2025)

	Ref	Expression
Assertion	onsupeqnmax	$$⊢A\subseteq \mathrm{On}\to \left(\forall x\in A\exists y\in Ax\in y\leftrightarrow \left(\bigcup A=\bigcup \bigcup A\wedge \neg \bigcup A\in A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(A\subseteq \mathrm{On}\wedge x\in A\right)\to A\subseteq \mathrm{On}$$
2	1	sselda	$$⊢\left(\left(A\subseteq \mathrm{On}\wedge x\in A\right)\wedge y\in A\right)\to y\in \mathrm{On}$$
3		ssel2	$$⊢\left(A\subseteq \mathrm{On}\wedge x\in A\right)\to x\in \mathrm{On}$$
4	3	adantr	$$⊢\left(\left(A\subseteq \mathrm{On}\wedge x\in A\right)\wedge y\in A\right)\to x\in \mathrm{On}$$
5		ontri1	$$⊢\left(y\in \mathrm{On}\wedge x\in \mathrm{On}\right)\to \left(y\subseteq x\leftrightarrow \neg x\in y\right)$$
6	2 4 5	syl2anc	$$⊢\left(\left(A\subseteq \mathrm{On}\wedge x\in A\right)\wedge y\in A\right)\to \left(y\subseteq x\leftrightarrow \neg x\in y\right)$$
7	6	ralbidva	$$⊢\left(A\subseteq \mathrm{On}\wedge x\in A\right)\to \left(\forall y\in Ay\subseteq x\leftrightarrow \forall y\in A\neg x\in y\right)$$
8	7	rexbidva	$$⊢A\subseteq \mathrm{On}\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)$$
9	8	notbid	$$⊢A\subseteq \mathrm{On}\to \left(\neg \exists x\in A\forall y\in Ay\subseteq x\leftrightarrow \neg \exists x\in A\forall y\in A\neg x\in y\right)$$
10	9	bicomd	$$⊢A\subseteq \mathrm{On}\to \left(\neg \exists x\in A\forall y\in A\neg x\in y\leftrightarrow \neg \exists x\in A\forall y\in Ay\subseteq x\right)$$
11		dfrex2	$$⊢\exists y\in Ax\in y\leftrightarrow \neg \forall y\in A\neg x\in y$$
12	11	ralbii	$$⊢\forall x\in A\exists y\in Ax\in y\leftrightarrow \forall x\in A\neg \forall y\in A\neg x\in y$$
13		ralnex	$$⊢\forall x\in A\neg \forall y\in A\neg x\in y\leftrightarrow \neg \exists x\in A\forall y\in A\neg x\in y$$
14	12 13	bitri	$$⊢\forall x\in A\exists y\in Ax\in y\leftrightarrow \neg \exists x\in A\forall y\in A\neg x\in y$$
15		unielid	$$⊢\bigcup A\in A\leftrightarrow \exists x\in A\forall y\in Ay\subseteq x$$
16	15	notbii	$$⊢\neg \bigcup A\in A\leftrightarrow \neg \exists x\in A\forall y\in Ay\subseteq x$$
17	10 14 16	3bitr4g	$$⊢A\subseteq \mathrm{On}\to \left(\forall x\in A\exists y\in Ax\in y\leftrightarrow \neg \bigcup A\in A\right)$$
18		onsupnmax	$$⊢A\subseteq \mathrm{On}\to \left(\neg \bigcup A\in A\to \bigcup A=\bigcup \bigcup A\right)$$
19	18	pm4.71rd	$$⊢A\subseteq \mathrm{On}\to \left(\neg \bigcup A\in A\leftrightarrow \left(\bigcup A=\bigcup \bigcup A\wedge \neg \bigcup A\in A\right)\right)$$
20	17 19	bitrd	$$⊢A\subseteq \mathrm{On}\to \left(\forall x\in A\exists y\in Ax\in y\leftrightarrow \left(\bigcup A=\bigcup \bigcup A\wedge \neg \bigcup A\in A\right)\right)$$