suplem1pr

Description: The union of a nonempty, bounded set of positive reals is a positive real. Part of Proposition 9-3.3 of Gleason p. 122. (Contributed by NM, 19-May-1996) (Revised by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	suplem1pr	$⊢ (A \neq \emptyset \land \exists x \in 𝑷 \forall y \in A y <_{𝑷} x) \to ⋃ A \in 𝑷$

Proof

Step	Hyp	Ref	Expression
1		ltrelpr	$⊢ <_{𝑷} \subseteq 𝑷 \times 𝑷$
2	1	brel	$⊢ y <_{𝑷} x \to (y \in 𝑷 \land x \in 𝑷)$
3	2	simpld	$⊢ y <_{𝑷} x \to y \in 𝑷$
4	3	ralimi	$⊢ \forall y \in A y <_{𝑷} x \to \forall y \in A y \in 𝑷$
5		dfss3	$⊢ A \subseteq 𝑷 \leftrightarrow \forall y \in A y \in 𝑷$
6	4 5	sylibr	$⊢ \forall y \in A y <_{𝑷} x \to A \subseteq 𝑷$
7	6	rexlimivw	$⊢ \exists x \in 𝑷 \forall y \in A y <_{𝑷} x \to A \subseteq 𝑷$
8	7	adantl	$⊢ (A \neq \emptyset \land \exists x \in 𝑷 \forall y \in A y <_{𝑷} x) \to A \subseteq 𝑷$
9		n0	$⊢ A \neq \emptyset \leftrightarrow \exists z z \in A$
10		ssel	$⊢ A \subseteq 𝑷 \to (z \in A \to z \in 𝑷)$
11		prn0	$⊢ z \in 𝑷 \to z \neq \emptyset$
12		0pss	$⊢ \emptyset \subset z \leftrightarrow z \neq \emptyset$
13	11 12	sylibr	$⊢ z \in 𝑷 \to \emptyset \subset z$
14		elssuni	$⊢ z \in A \to z \subseteq ⋃ A$
15		psssstr	$⊢ (\emptyset \subset z \land z \subseteq ⋃ A) \to \emptyset \subset ⋃ A$
16	13 14 15	syl2an	$⊢ (z \in 𝑷 \land z \in A) \to \emptyset \subset ⋃ A$
17	16	expcom	$⊢ z \in A \to (z \in 𝑷 \to \emptyset \subset ⋃ A)$
18	10 17	sylcom	$⊢ A \subseteq 𝑷 \to (z \in A \to \emptyset \subset ⋃ A)$
19	18	exlimdv	$⊢ A \subseteq 𝑷 \to (\exists z z \in A \to \emptyset \subset ⋃ A)$
20	9 19	syl5bi	$⊢ A \subseteq 𝑷 \to (A \neq \emptyset \to \emptyset \subset ⋃ A)$
21		prpssnq	$⊢ x \in 𝑷 \to x \subset 𝑸$
22	21	adantl	$⊢ (A \subseteq 𝑷 \land x \in 𝑷) \to x \subset 𝑸$
23		ltprord	$⊢ (y \in 𝑷 \land x \in 𝑷) \to (y <_{𝑷} x \leftrightarrow y \subset x)$
24		pssss	$⊢ y \subset x \to y \subseteq x$
25	23 24	syl6bi	$⊢ (y \in 𝑷 \land x \in 𝑷) \to (y <_{𝑷} x \to y \subseteq x)$
26	2 25	mpcom	$⊢ y <_{𝑷} x \to y \subseteq x$
27	26	ralimi	$⊢ \forall y \in A y <_{𝑷} x \to \forall y \in A y \subseteq x$
28		unissb	$⊢ ⋃ A \subseteq x \leftrightarrow \forall y \in A y \subseteq x$
29	27 28	sylibr	$⊢ \forall y \in A y <_{𝑷} x \to ⋃ A \subseteq x$
30		sspsstr	$⊢ (⋃ A \subseteq x \land x \subset 𝑸) \to ⋃ A \subset 𝑸$
31	30	expcom	$⊢ x \subset 𝑸 \to (⋃ A \subseteq x \to ⋃ A \subset 𝑸)$
32	22 29 31	syl2im	$⊢ (A \subseteq 𝑷 \land x \in 𝑷) \to (\forall y \in A y <_{𝑷} x \to ⋃ A \subset 𝑸)$
33	32	rexlimdva	$⊢ A \subseteq 𝑷 \to (\exists x \in 𝑷 \forall y \in A y <_{𝑷} x \to ⋃ A \subset 𝑸)$
34	20 33	anim12d	$⊢ A \subseteq 𝑷 \to ((A \neq \emptyset \land \exists x \in 𝑷 \forall y \in A y <_{𝑷} x) \to (\emptyset \subset ⋃ A \land ⋃ A \subset 𝑸))$
35	8 34	mpcom	$⊢ (A \neq \emptyset \land \exists x \in 𝑷 \forall y \in A y <_{𝑷} x) \to (\emptyset \subset ⋃ A \land ⋃ A \subset 𝑸)$
36		prcdnq	$⊢ (z \in 𝑷 \land x \in z) \to (y <_{𝑸} x \to y \in z)$
37	36	ex	$⊢ z \in 𝑷 \to (x \in z \to (y <_{𝑸} x \to y \in z))$
38	37	com3r	$⊢ y <_{𝑸} x \to (z \in 𝑷 \to (x \in z \to y \in z))$
39	10 38	sylan9	$⊢ (A \subseteq 𝑷 \land y <_{𝑸} x) \to (z \in A \to (x \in z \to y \in z))$
40	39	reximdvai	$⊢ (A \subseteq 𝑷 \land y <_{𝑸} x) \to (\exists z \in A x \in z \to \exists z \in A y \in z)$
41		eluni2	$⊢ x \in ⋃ A \leftrightarrow \exists z \in A x \in z$
42		eluni2	$⊢ y \in ⋃ A \leftrightarrow \exists z \in A y \in z$
43	40 41 42	3imtr4g	$⊢ (A \subseteq 𝑷 \land y <_{𝑸} x) \to (x \in ⋃ A \to y \in ⋃ A)$
44	43	ex	$⊢ A \subseteq 𝑷 \to (y <_{𝑸} x \to (x \in ⋃ A \to y \in ⋃ A))$
45	44	com23	$⊢ A \subseteq 𝑷 \to (x \in ⋃ A \to (y <_{𝑸} x \to y \in ⋃ A))$
46	45	alrimdv	$⊢ A \subseteq 𝑷 \to (x \in ⋃ A \to \forall y (y <_{𝑸} x \to y \in ⋃ A))$
47		eluni	$⊢ x \in ⋃ A \leftrightarrow \exists z (x \in z \land z \in A)$
48		prnmax	$⊢ (z \in 𝑷 \land x \in z) \to \exists y \in z x <_{𝑸} y$
49	48	ex	$⊢ z \in 𝑷 \to (x \in z \to \exists y \in z x <_{𝑸} y)$
50	10 49	syl6	$⊢ A \subseteq 𝑷 \to (z \in A \to (x \in z \to \exists y \in z x <_{𝑸} y))$
51	50	com23	$⊢ A \subseteq 𝑷 \to (x \in z \to (z \in A \to \exists y \in z x <_{𝑸} y))$
52	51	imp	$⊢ (A \subseteq 𝑷 \land x \in z) \to (z \in A \to \exists y \in z x <_{𝑸} y)$
53		ssrexv	$⊢ z \subseteq ⋃ A \to (\exists y \in z x <_{𝑸} y \to \exists y \in ⋃ A x <_{𝑸} y)$
54	14 53	syl	$⊢ z \in A \to (\exists y \in z x <_{𝑸} y \to \exists y \in ⋃ A x <_{𝑸} y)$
55	52 54	sylcom	$⊢ (A \subseteq 𝑷 \land x \in z) \to (z \in A \to \exists y \in ⋃ A x <_{𝑸} y)$
56	55	expimpd	$⊢ A \subseteq 𝑷 \to ((x \in z \land z \in A) \to \exists y \in ⋃ A x <_{𝑸} y)$
57	56	exlimdv	$⊢ A \subseteq 𝑷 \to (\exists z (x \in z \land z \in A) \to \exists y \in ⋃ A x <_{𝑸} y)$
58	47 57	syl5bi	$⊢ A \subseteq 𝑷 \to (x \in ⋃ A \to \exists y \in ⋃ A x <_{𝑸} y)$
59	46 58	jcad	$⊢ A \subseteq 𝑷 \to (x \in ⋃ A \to (\forall y (y <_{𝑸} x \to y \in ⋃ A) \land \exists y \in ⋃ A x <_{𝑸} y))$
60	59	ralrimiv	$⊢ A \subseteq 𝑷 \to \forall x \in ⋃ A (\forall y (y <_{𝑸} x \to y \in ⋃ A) \land \exists y \in ⋃ A x <_{𝑸} y)$
61	8 60	syl	$⊢ (A \neq \emptyset \land \exists x \in 𝑷 \forall y \in A y <_{𝑷} x) \to \forall x \in ⋃ A (\forall y (y <_{𝑸} x \to y \in ⋃ A) \land \exists y \in ⋃ A x <_{𝑸} y)$
62		elnp	$⊢ ⋃ A \in 𝑷 \leftrightarrow ((\emptyset \subset ⋃ A \land ⋃ A \subset 𝑸) \land \forall x \in ⋃ A (\forall y (y <_{𝑸} x \to y \in ⋃ A) \land \exists y \in ⋃ A x <_{𝑸} y))$
63	35 61 62	sylanbrc	$⊢ (A \neq \emptyset \land \exists x \in 𝑷 \forall y \in A y <_{𝑷} x) \to ⋃ A \in 𝑷$

Metamath Proof Explorer

Theorem suplem1pr

Proof