suplem2pr

Description: The union of a set of positive reals (if a positive real) is its supremum (the least upper bound). 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	suplem2pr	$⊢ A \subseteq 𝑷 \to ((y \in A \to \neg ⋃ A <_{𝑷} y) \land (y <_{𝑷} ⋃ A \to \exists z \in A y <_{𝑷} z))$

Proof

Step	Hyp	Ref	Expression
1		ltrelpr	$⊢ <_{𝑷} \subseteq 𝑷 \times 𝑷$
2	1	brel	$⊢ y <_{𝑷} ⋃ A \to (y \in 𝑷 \land ⋃ A \in 𝑷)$
3	2	simpld	$⊢ y <_{𝑷} ⋃ A \to y \in 𝑷$
4		ralnex	$⊢ \forall z \in A \neg y <_{𝑷} z \leftrightarrow \neg \exists z \in A y <_{𝑷} z$
5		ssel2	$⊢ (A \subseteq 𝑷 \land z \in A) \to z \in 𝑷$
6		ltsopr	$⊢ <_{𝑷} Or 𝑷$
7		sotric	$⊢ (<_{𝑷} Or 𝑷 \land (y \in 𝑷 \land z \in 𝑷)) \to (y <_{𝑷} z \leftrightarrow \neg (y = z \lor z <_{𝑷} y))$
8	6 7	mpan	$⊢ (y \in 𝑷 \land z \in 𝑷) \to (y <_{𝑷} z \leftrightarrow \neg (y = z \lor z <_{𝑷} y))$
9	8	con2bid	$⊢ (y \in 𝑷 \land z \in 𝑷) \to ((y = z \lor z <_{𝑷} y) \leftrightarrow \neg y <_{𝑷} z)$
10	9	ancoms	$⊢ (z \in 𝑷 \land y \in 𝑷) \to ((y = z \lor z <_{𝑷} y) \leftrightarrow \neg y <_{𝑷} z)$
11		ltprord	$⊢ (z \in 𝑷 \land y \in 𝑷) \to (z <_{𝑷} y \leftrightarrow z \subset y)$
12	11	orbi2d	$⊢ (z \in 𝑷 \land y \in 𝑷) \to ((y = z \lor z <_{𝑷} y) \leftrightarrow (y = z \lor z \subset y))$
13		sspss	$⊢ z \subseteq y \leftrightarrow (z \subset y \lor z = y)$
14		equcom	$⊢ z = y \leftrightarrow y = z$
15	14	orbi2i	$⊢ (z \subset y \lor z = y) \leftrightarrow (z \subset y \lor y = z)$
16		orcom	$⊢ (z \subset y \lor y = z) \leftrightarrow (y = z \lor z \subset y)$
17	13 15 16	3bitri	$⊢ z \subseteq y \leftrightarrow (y = z \lor z \subset y)$
18	12 17	bitr4di	$⊢ (z \in 𝑷 \land y \in 𝑷) \to ((y = z \lor z <_{𝑷} y) \leftrightarrow z \subseteq y)$
19	10 18	bitr3d	$⊢ (z \in 𝑷 \land y \in 𝑷) \to (\neg y <_{𝑷} z \leftrightarrow z \subseteq y)$
20	5 19	sylan	$⊢ ((A \subseteq 𝑷 \land z \in A) \land y \in 𝑷) \to (\neg y <_{𝑷} z \leftrightarrow z \subseteq y)$
21	20	an32s	$⊢ ((A \subseteq 𝑷 \land y \in 𝑷) \land z \in A) \to (\neg y <_{𝑷} z \leftrightarrow z \subseteq y)$
22	21	ralbidva	$⊢ (A \subseteq 𝑷 \land y \in 𝑷) \to (\forall z \in A \neg y <_{𝑷} z \leftrightarrow \forall z \in A z \subseteq y)$
23	4 22	bitr3id	$⊢ (A \subseteq 𝑷 \land y \in 𝑷) \to (\neg \exists z \in A y <_{𝑷} z \leftrightarrow \forall z \in A z \subseteq y)$
24		unissb	$⊢ ⋃ A \subseteq y \leftrightarrow \forall z \in A z \subseteq y$
25	23 24	bitr4di	$⊢ (A \subseteq 𝑷 \land y \in 𝑷) \to (\neg \exists z \in A y <_{𝑷} z \leftrightarrow ⋃ A \subseteq y)$
26		ssnpss	$⊢ ⋃ A \subseteq y \to \neg y \subset ⋃ A$
27		ltprord	$⊢ (y \in 𝑷 \land ⋃ A \in 𝑷) \to (y <_{𝑷} ⋃ A \leftrightarrow y \subset ⋃ A)$
28	27	biimpd	$⊢ (y \in 𝑷 \land ⋃ A \in 𝑷) \to (y <_{𝑷} ⋃ A \to y \subset ⋃ A)$
29	2 28	mpcom	$⊢ y <_{𝑷} ⋃ A \to y \subset ⋃ A$
30	26 29	nsyl	$⊢ ⋃ A \subseteq y \to \neg y <_{𝑷} ⋃ A$
31	25 30	biimtrdi	$⊢ (A \subseteq 𝑷 \land y \in 𝑷) \to (\neg \exists z \in A y <_{𝑷} z \to \neg y <_{𝑷} ⋃ A)$
32	31	con4d	$⊢ (A \subseteq 𝑷 \land y \in 𝑷) \to (y <_{𝑷} ⋃ A \to \exists z \in A y <_{𝑷} z)$
33	32	ex	$⊢ A \subseteq 𝑷 \to (y \in 𝑷 \to (y <_{𝑷} ⋃ A \to \exists z \in A y <_{𝑷} z))$
34	3 33	syl5	$⊢ A \subseteq 𝑷 \to (y <_{𝑷} ⋃ A \to (y <_{𝑷} ⋃ A \to \exists z \in A y <_{𝑷} z))$
35	34	pm2.43d	$⊢ A \subseteq 𝑷 \to (y <_{𝑷} ⋃ A \to \exists z \in A y <_{𝑷} z)$
36		elssuni	$⊢ y \in A \to y \subseteq ⋃ A$
37		ssnpss	$⊢ y \subseteq ⋃ A \to \neg ⋃ A \subset y$
38	36 37	syl	$⊢ y \in A \to \neg ⋃ A \subset y$
39	1	brel	$⊢ ⋃ A <_{𝑷} y \to (⋃ A \in 𝑷 \land y \in 𝑷)$
40		ltprord	$⊢ (⋃ A \in 𝑷 \land y \in 𝑷) \to (⋃ A <_{𝑷} y \leftrightarrow ⋃ A \subset y)$
41	40	biimpd	$⊢ (⋃ A \in 𝑷 \land y \in 𝑷) \to (⋃ A <_{𝑷} y \to ⋃ A \subset y)$
42	39 41	mpcom	$⊢ ⋃ A <_{𝑷} y \to ⋃ A \subset y$
43	38 42	nsyl	$⊢ y \in A \to \neg ⋃ A <_{𝑷} y$
44	35 43	jctil	$⊢ A \subseteq 𝑷 \to ((y \in A \to \neg ⋃ A <_{𝑷} y) \land (y <_{𝑷} ⋃ A \to \exists z \in A y <_{𝑷} z))$

Metamath Proof Explorer

Theorem suplem2pr

Proof