Theorem supexpr

Description: The union of a nonempty, bounded set of positive reals has a supremum. Part of Proposition 9-3.3 of Gleason p. 122. (Contributed by NM, 19-May-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	supexpr	$$⊢\left(A\ne \varnothing \wedge \exists x\in 𝑷\forall y\in Ay{<}_{𝑷}x\right)\to \exists x\in 𝑷\left(\forall y\in A\neg x{<}_{𝑷}y\wedge \forall y\in 𝑷\left(y{<}_{𝑷}x\to \exists z\in Ay{<}_{𝑷}z\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		suplem1pr	$$⊢\left(A\ne \varnothing \wedge \exists x\in 𝑷\forall y\in Ay{<}_{𝑷}x\right)\to \bigcup A\in 𝑷$$
2		ltrelpr	$$⊢{<}_{𝑷}\subseteq 𝑷\times 𝑷$$
3	2	brel	$$⊢y{<}_{𝑷}x\to \left(y\in 𝑷\wedge x\in 𝑷\right)$$
4	3	simpld	$$⊢y{<}_{𝑷}x\to y\in 𝑷$$
5	4	ralimi	$$⊢\forall y\in Ay{<}_{𝑷}x\to \forall y\in Ay\in 𝑷$$
6		dfss3	$$⊢A\subseteq 𝑷\leftrightarrow \forall y\in Ay\in 𝑷$$
7	5 6	sylibr	$$⊢\forall y\in Ay{<}_{𝑷}x\to A\subseteq 𝑷$$
8	7	rexlimivw	$$⊢\exists x\in 𝑷\forall y\in Ay{<}_{𝑷}x\to A\subseteq 𝑷$$
9	8	adantl	$$⊢\left(A\ne \varnothing \wedge \exists x\in 𝑷\forall y\in Ay{<}_{𝑷}x\right)\to A\subseteq 𝑷$$
10		suplem2pr	$$⊢A\subseteq 𝑷\to \left(\left(y\in A\to \neg \bigcup A{<}_{𝑷}y\right)\wedge \left(y{<}_{𝑷}\bigcup A\to \exists z\in Ay{<}_{𝑷}z\right)\right)$$
11	10	simpld	$$⊢A\subseteq 𝑷\to \left(y\in A\to \neg \bigcup A{<}_{𝑷}y\right)$$
12	11	ralrimiv	$$⊢A\subseteq 𝑷\to \forall y\in A\neg \bigcup A{<}_{𝑷}y$$
13	10	simprd	$$⊢A\subseteq 𝑷\to \left(y{<}_{𝑷}\bigcup A\to \exists z\in Ay{<}_{𝑷}z\right)$$
14	13	ralrimivw	$$⊢A\subseteq 𝑷\to \forall y\in 𝑷\left(y{<}_{𝑷}\bigcup A\to \exists z\in Ay{<}_{𝑷}z\right)$$
15	12 14	jca	$$⊢A\subseteq 𝑷\to \left(\forall y\in A\neg \bigcup A{<}_{𝑷}y\wedge \forall y\in 𝑷\left(y{<}_{𝑷}\bigcup A\to \exists z\in Ay{<}_{𝑷}z\right)\right)$$
16	9 15	syl	$$⊢\left(A\ne \varnothing \wedge \exists x\in 𝑷\forall y\in Ay{<}_{𝑷}x\right)\to \left(\forall y\in A\neg \bigcup A{<}_{𝑷}y\wedge \forall y\in 𝑷\left(y{<}_{𝑷}\bigcup A\to \exists z\in Ay{<}_{𝑷}z\right)\right)$$
17		breq1	$$⊢x=\bigcup A\to \left(x{<}_{𝑷}y\leftrightarrow \bigcup A{<}_{𝑷}y\right)$$
18	17	notbid	$$⊢x=\bigcup A\to \left(\neg x{<}_{𝑷}y\leftrightarrow \neg \bigcup A{<}_{𝑷}y\right)$$
19	18	ralbidv	$$⊢x=\bigcup A\to \left(\forall y\in A\neg x{<}_{𝑷}y\leftrightarrow \forall y\in A\neg \bigcup A{<}_{𝑷}y\right)$$
20		breq2	$$⊢x=\bigcup A\to \left(y{<}_{𝑷}x\leftrightarrow y{<}_{𝑷}\bigcup A\right)$$
21	20	imbi1d	$$⊢x=\bigcup A\to \left(\left(y{<}_{𝑷}x\to \exists z\in Ay{<}_{𝑷}z\right)\leftrightarrow \left(y{<}_{𝑷}\bigcup A\to \exists z\in Ay{<}_{𝑷}z\right)\right)$$
22	21	ralbidv	$$⊢x=\bigcup A\to \left(\forall y\in 𝑷\left(y{<}_{𝑷}x\to \exists z\in Ay{<}_{𝑷}z\right)\leftrightarrow \forall y\in 𝑷\left(y{<}_{𝑷}\bigcup A\to \exists z\in Ay{<}_{𝑷}z\right)\right)$$
23	19 22	anbi12d	$$⊢x=\bigcup A\to \left(\left(\forall y\in A\neg x{<}_{𝑷}y\wedge \forall y\in 𝑷\left(y{<}_{𝑷}x\to \exists z\in Ay{<}_{𝑷}z\right)\right)\leftrightarrow \left(\forall y\in A\neg \bigcup A{<}_{𝑷}y\wedge \forall y\in 𝑷\left(y{<}_{𝑷}\bigcup A\to \exists z\in Ay{<}_{𝑷}z\right)\right)\right)$$
24	23	rspcev	$$⊢\left(\bigcup A\in 𝑷\wedge \left(\forall y\in A\neg \bigcup A{<}_{𝑷}y\wedge \forall y\in 𝑷\left(y{<}_{𝑷}\bigcup A\to \exists z\in Ay{<}_{𝑷}z\right)\right)\right)\to \exists x\in 𝑷\left(\forall y\in A\neg x{<}_{𝑷}y\wedge \forall y\in 𝑷\left(y{<}_{𝑷}x\to \exists z\in Ay{<}_{𝑷}z\right)\right)$$
25	1 16 24	syl2anc	$$⊢\left(A\ne \varnothing \wedge \exists x\in 𝑷\forall y\in Ay{<}_{𝑷}x\right)\to \exists x\in 𝑷\left(\forall y\in A\neg x{<}_{𝑷}y\wedge \forall y\in 𝑷\left(y{<}_{𝑷}x\to \exists z\in Ay{<}_{𝑷}z\right)\right)$$