Theorem sorpssint

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

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

Proof

Step	Hyp	Ref	Expression
1		intss1	$$⊢u\in Y\to \bigcap Y\subseteq u$$
2	1	3ad2ant2	$$⊢\left([\subset ]\mathrm{Or}Y\wedge u\in Y\wedge \forall v\in Y\neg v\subset u\right)\to \bigcap Y\subseteq u$$
3		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)$$
4	3	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)$$
5		sspss	$$⊢v\subseteq u\leftrightarrow \left(v\subset u\vee v=u\right)$$
6		orel1	$$⊢\neg v\subset u\to \left(\left(v\subset u\vee v=u\right)\to v=u\right)$$
7		eqimss2	$$⊢v=u\to u\subseteq v$$
8	6 7	syl6com	$$⊢\left(v\subset u\vee v=u\right)\to \left(\neg v\subset u\to u\subseteq v\right)$$
9	5 8	sylbi	$$⊢v\subseteq u\to \left(\neg v\subset u\to u\subseteq v\right)$$
10	9	jao1i	$$⊢\left(u\subseteq v\vee v\subseteq u\right)\to \left(\neg v\subset u\to u\subseteq v\right)$$
11	4 10	syl	$$⊢\left(\left([\subset ]\mathrm{Or}Y\wedge u\in Y\right)\wedge v\in Y\right)\to \left(\neg v\subset u\to u\subseteq v\right)$$
12	11	ralimdva	$$⊢\left([\subset ]\mathrm{Or}Y\wedge u\in Y\right)\to \left(\forall v\in Y\neg v\subset u\to \forall v\in Yu\subseteq v\right)$$
13	12	3impia	$$⊢\left([\subset ]\mathrm{Or}Y\wedge u\in Y\wedge \forall v\in Y\neg v\subset u\right)\to \forall v\in Yu\subseteq v$$
14		ssint	$$⊢u\subseteq \bigcap Y\leftrightarrow \forall v\in Yu\subseteq v$$
15	13 14	sylibr	$$⊢\left([\subset ]\mathrm{Or}Y\wedge u\in Y\wedge \forall v\in Y\neg v\subset u\right)\to u\subseteq \bigcap Y$$
16	2 15	eqssd	$$⊢\left([\subset ]\mathrm{Or}Y\wedge u\in Y\wedge \forall v\in Y\neg v\subset u\right)\to \bigcap Y=u$$
17		simp2	$$⊢\left([\subset ]\mathrm{Or}Y\wedge u\in Y\wedge \forall v\in Y\neg v\subset u\right)\to u\in Y$$
18	16 17	eqeltrd	$$⊢\left([\subset ]\mathrm{Or}Y\wedge u\in Y\wedge \forall v\in Y\neg v\subset u\right)\to \bigcap Y\in Y$$
19	18	rexlimdv3a	$$⊢[\subset ]\mathrm{Or}Y\to \left(\exists u\in Y\forall v\in Y\neg v\subset u\to \bigcap Y\in Y\right)$$
20		intss1	$$⊢v\in Y\to \bigcap Y\subseteq v$$
21		ssnpss	$$⊢\bigcap Y\subseteq v\to \neg v\subset \bigcap Y$$
22	20 21	syl	$$⊢v\in Y\to \neg v\subset \bigcap Y$$
23	22	rgen	$$⊢\forall v\in Y\neg v\subset \bigcap Y$$
24		psseq2	$$⊢u=\bigcap Y\to \left(v\subset u\leftrightarrow v\subset \bigcap Y\right)$$
25	24	notbid	$$⊢u=\bigcap Y\to \left(\neg v\subset u\leftrightarrow \neg v\subset \bigcap Y\right)$$
26	25	ralbidv	$$⊢u=\bigcap Y\to \left(\forall v\in Y\neg v\subset u\leftrightarrow \forall v\in Y\neg v\subset \bigcap Y\right)$$
27	26	rspcev	$$⊢\left(\bigcap Y\in Y\wedge \forall v\in Y\neg v\subset \bigcap Y\right)\to \exists u\in Y\forall v\in Y\neg v\subset u$$
28	23 27	mpan2	$$⊢\bigcap Y\in Y\to \exists u\in Y\forall v\in Y\neg v\subset u$$
29	19 28	impbid1	$$⊢[\subset ]\mathrm{Or}Y\to \left(\exists u\in Y\forall v\in Y\neg v\subset u\leftrightarrow \bigcap Y\in Y\right)$$