Theorem sorpssuni

Description: In a chain of sets, a maximal element is the union of the chain. (Contributed by Stefan O'Rear, 2-Nov-2014)

	Ref	Expression
Assertion	sorpssuni	$$⊢[\subset ]\mathrm{Or}Y\to \left(\exists u\in Y\forall v\in Y\neg u\subset v\leftrightarrow \bigcup Y\in Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		sorpssi	$$⊢\left([\subset ]\mathrm{Or}Y\wedge \left(u\in Y\wedge v\in Y\right)\right)\to \left(u\subseteq v\vee v\subseteq u\right)$$
2	1	anassrs	$$⊢\left(\left([\subset ]\mathrm{Or}Y\wedge u\in Y\right)\wedge v\in Y\right)\to \left(u\subseteq v\vee v\subseteq u\right)$$
3		sspss	$$⊢u\subseteq v\leftrightarrow \left(u\subset v\vee u=v\right)$$
4		orel1	$$⊢\neg u\subset v\to \left(\left(u\subset v\vee u=v\right)\to u=v\right)$$
5		eqimss2	$$⊢u=v\to v\subseteq u$$
6	4 5	syl6com	$$⊢\left(u\subset v\vee u=v\right)\to \left(\neg u\subset v\to v\subseteq u\right)$$
7	3 6	sylbi	$$⊢u\subseteq v\to \left(\neg u\subset v\to v\subseteq u\right)$$
8		ax-1	$$⊢v\subseteq u\to \left(\neg u\subset v\to v\subseteq u\right)$$
9	7 8	jaoi	$$⊢\left(u\subseteq v\vee v\subseteq u\right)\to \left(\neg u\subset v\to v\subseteq u\right)$$
10	2 9	syl	$$⊢\left(\left([\subset ]\mathrm{Or}Y\wedge u\in Y\right)\wedge v\in Y\right)\to \left(\neg u\subset v\to v\subseteq u\right)$$
11	10	ralimdva	$$⊢\left([\subset ]\mathrm{Or}Y\wedge u\in Y\right)\to \left(\forall v\in Y\neg u\subset v\to \forall v\in Yv\subseteq u\right)$$
12	11	3impia	$$⊢\left([\subset ]\mathrm{Or}Y\wedge u\in Y\wedge \forall v\in Y\neg u\subset v\right)\to \forall v\in Yv\subseteq u$$
13		unissb	$$⊢\bigcup Y\subseteq u\leftrightarrow \forall v\in Yv\subseteq u$$
14	12 13	sylibr	$$⊢\left([\subset ]\mathrm{Or}Y\wedge u\in Y\wedge \forall v\in Y\neg u\subset v\right)\to \bigcup Y\subseteq u$$
15		elssuni	$$⊢u\in Y\to u\subseteq \bigcup Y$$
16	15	3ad2ant2	$$⊢\left([\subset ]\mathrm{Or}Y\wedge u\in Y\wedge \forall v\in Y\neg u\subset v\right)\to u\subseteq \bigcup Y$$
17	14 16	eqssd	$$⊢\left([\subset ]\mathrm{Or}Y\wedge u\in Y\wedge \forall v\in Y\neg u\subset v\right)\to \bigcup Y=u$$
18		simp2	$$⊢\left([\subset ]\mathrm{Or}Y\wedge u\in Y\wedge \forall v\in Y\neg u\subset v\right)\to u\in Y$$
19	17 18	eqeltrd	$$⊢\left([\subset ]\mathrm{Or}Y\wedge u\in Y\wedge \forall v\in Y\neg u\subset v\right)\to \bigcup Y\in Y$$
20	19	rexlimdv3a	$$⊢[\subset ]\mathrm{Or}Y\to \left(\exists u\in Y\forall v\in Y\neg u\subset v\to \bigcup Y\in Y\right)$$
21		elssuni	$$⊢v\in Y\to v\subseteq \bigcup Y$$
22		ssnpss	$$⊢v\subseteq \bigcup Y\to \neg \bigcup Y\subset v$$
23	21 22	syl	$$⊢v\in Y\to \neg \bigcup Y\subset v$$
24	23	rgen	$$⊢\forall v\in Y\neg \bigcup Y\subset v$$
25		psseq1	$$⊢u=\bigcup Y\to \left(u\subset v\leftrightarrow \bigcup Y\subset v\right)$$
26	25	notbid	$$⊢u=\bigcup Y\to \left(\neg u\subset v\leftrightarrow \neg \bigcup Y\subset v\right)$$
27	26	ralbidv	$$⊢u=\bigcup Y\to \left(\forall v\in Y\neg u\subset v\leftrightarrow \forall v\in Y\neg \bigcup Y\subset v\right)$$
28	27	rspcev	$$⊢\left(\bigcup Y\in Y\wedge \forall v\in Y\neg \bigcup Y\subset v\right)\to \exists u\in Y\forall v\in Y\neg u\subset v$$
29	24 28	mpan2	$$⊢\bigcup Y\in Y\to \exists u\in Y\forall v\in Y\neg u\subset v$$
30	20 29	impbid1	$$⊢[\subset ]\mathrm{Or}Y\to \left(\exists u\in Y\forall v\in Y\neg u\subset v\leftrightarrow \bigcup Y\in Y\right)$$