Theorem 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	⊢ ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ P ∀ 𝑦 ∈ 𝐴 𝑦 <P 𝑥 ) → ∪ 𝐴 ∈ P )

Proof

Step	Hyp	Ref	Expression
1		ltrelpr	⊢ <P ⊆ ( P × P )
2	1	brel	⊢ ( 𝑦 <P 𝑥 → ( 𝑦 ∈ P ∧ 𝑥 ∈ P ) )
3	2	simpld	⊢ ( 𝑦 <P 𝑥 → 𝑦 ∈ P )
4	3	ralimi	⊢ ( ∀ 𝑦 ∈ 𝐴 𝑦 <P 𝑥 → ∀ 𝑦 ∈ 𝐴 𝑦 ∈ P )
5		dfss3	⊢ ( 𝐴 ⊆ P ↔ ∀ 𝑦 ∈ 𝐴 𝑦 ∈ P )
6	4 5	sylibr	⊢ ( ∀ 𝑦 ∈ 𝐴 𝑦 <P 𝑥 → 𝐴 ⊆ P )
7	6	rexlimivw	⊢ ( ∃ 𝑥 ∈ P ∀ 𝑦 ∈ 𝐴 𝑦 <P 𝑥 → 𝐴 ⊆ P )
8	7	adantl	⊢ ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ P ∀ 𝑦 ∈ 𝐴 𝑦 <P 𝑥 ) → 𝐴 ⊆ P )
9		n0	⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ 𝐴 )
10		ssel	⊢ ( 𝐴 ⊆ P → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ P ) )
11		prn0	⊢ ( 𝑧 ∈ P → 𝑧 ≠ ∅ )
12		0pss	⊢ ( ∅ ⊊ 𝑧 ↔ 𝑧 ≠ ∅ )
13	11 12	sylibr	⊢ ( 𝑧 ∈ P → ∅ ⊊ 𝑧 )
14		elssuni	⊢ ( 𝑧 ∈ 𝐴 → 𝑧 ⊆ ∪ 𝐴 )
15		psssstr	⊢ ( ( ∅ ⊊ 𝑧 ∧ 𝑧 ⊆ ∪ 𝐴 ) → ∅ ⊊ ∪ 𝐴 )
16	13 14 15	syl2an	⊢ ( ( 𝑧 ∈ P ∧ 𝑧 ∈ 𝐴 ) → ∅ ⊊ ∪ 𝐴 )
17	16	expcom	⊢ ( 𝑧 ∈ 𝐴 → ( 𝑧 ∈ P → ∅ ⊊ ∪ 𝐴 ) )
18	10 17	sylcom	⊢ ( 𝐴 ⊆ P → ( 𝑧 ∈ 𝐴 → ∅ ⊊ ∪ 𝐴 ) )
19	18	exlimdv	⊢ ( 𝐴 ⊆ P → ( ∃ 𝑧 𝑧 ∈ 𝐴 → ∅ ⊊ ∪ 𝐴 ) )
20	9 19	syl5bi	⊢ ( 𝐴 ⊆ P → ( 𝐴 ≠ ∅ → ∅ ⊊ ∪ 𝐴 ) )
21		prpssnq	⊢ ( 𝑥 ∈ P → 𝑥 ⊊ Q )
22	21	adantl	⊢ ( ( 𝐴 ⊆ P ∧ 𝑥 ∈ P ) → 𝑥 ⊊ Q )
23		ltprord	⊢ ( ( 𝑦 ∈ P ∧ 𝑥 ∈ P ) → ( 𝑦 <P 𝑥 ↔ 𝑦 ⊊ 𝑥 ) )
24		pssss	⊢ ( 𝑦 ⊊ 𝑥 → 𝑦 ⊆ 𝑥 )
25	23 24	syl6bi	⊢ ( ( 𝑦 ∈ P ∧ 𝑥 ∈ P ) → ( 𝑦 <P 𝑥 → 𝑦 ⊆ 𝑥 ) )
26	2 25	mpcom	⊢ ( 𝑦 <P 𝑥 → 𝑦 ⊆ 𝑥 )
27	26	ralimi	⊢ ( ∀ 𝑦 ∈ 𝐴 𝑦 <P 𝑥 → ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 )
28		unissb	⊢ ( ∪ 𝐴 ⊆ 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 )
29	27 28	sylibr	⊢ ( ∀ 𝑦 ∈ 𝐴 𝑦 <P 𝑥 → ∪ 𝐴 ⊆ 𝑥 )
30		sspsstr	⊢ ( ( ∪ 𝐴 ⊆ 𝑥 ∧ 𝑥 ⊊ Q ) → ∪ 𝐴 ⊊ Q )
31	30	expcom	⊢ ( 𝑥 ⊊ Q → ( ∪ 𝐴 ⊆ 𝑥 → ∪ 𝐴 ⊊ Q ) )
32	22 29 31	syl2im	⊢ ( ( 𝐴 ⊆ P ∧ 𝑥 ∈ P ) → ( ∀ 𝑦 ∈ 𝐴 𝑦 <P 𝑥 → ∪ 𝐴 ⊊ Q ) )
33	32	rexlimdva	⊢ ( 𝐴 ⊆ P → ( ∃ 𝑥 ∈ P ∀ 𝑦 ∈ 𝐴 𝑦 <P 𝑥 → ∪ 𝐴 ⊊ Q ) )
34	20 33	anim12d	⊢ ( 𝐴 ⊆ P → ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ P ∀ 𝑦 ∈ 𝐴 𝑦 <P 𝑥 ) → ( ∅ ⊊ ∪ 𝐴 ∧ ∪ 𝐴 ⊊ Q ) ) )
35	8 34	mpcom	⊢ ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ P ∀ 𝑦 ∈ 𝐴 𝑦 <P 𝑥 ) → ( ∅ ⊊ ∪ 𝐴 ∧ ∪ 𝐴 ⊊ Q ) )
36		prcdnq	⊢ ( ( 𝑧 ∈ P ∧ 𝑥 ∈ 𝑧 ) → ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝑧 ) )
37	36	ex	⊢ ( 𝑧 ∈ P → ( 𝑥 ∈ 𝑧 → ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝑧 ) ) )
38	37	com3r	⊢ ( 𝑦 <Q 𝑥 → ( 𝑧 ∈ P → ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧 ) ) )
39	10 38	sylan9	⊢ ( ( 𝐴 ⊆ P ∧ 𝑦 <Q 𝑥 ) → ( 𝑧 ∈ 𝐴 → ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧 ) ) )
40	39	reximdvai	⊢ ( ( 𝐴 ⊆ P ∧ 𝑦 <Q 𝑥 ) → ( ∃ 𝑧 ∈ 𝐴 𝑥 ∈ 𝑧 → ∃ 𝑧 ∈ 𝐴 𝑦 ∈ 𝑧 ) )
41		eluni2	⊢ ( 𝑥 ∈ ∪ 𝐴 ↔ ∃ 𝑧 ∈ 𝐴 𝑥 ∈ 𝑧 )
42		eluni2	⊢ ( 𝑦 ∈ ∪ 𝐴 ↔ ∃ 𝑧 ∈ 𝐴 𝑦 ∈ 𝑧 )
43	40 41 42	3imtr4g	⊢ ( ( 𝐴 ⊆ P ∧ 𝑦 <Q 𝑥 ) → ( 𝑥 ∈ ∪ 𝐴 → 𝑦 ∈ ∪ 𝐴 ) )
44	43	ex	⊢ ( 𝐴 ⊆ P → ( 𝑦 <Q 𝑥 → ( 𝑥 ∈ ∪ 𝐴 → 𝑦 ∈ ∪ 𝐴 ) ) )
45	44	com23	⊢ ( 𝐴 ⊆ P → ( 𝑥 ∈ ∪ 𝐴 → ( 𝑦 <Q 𝑥 → 𝑦 ∈ ∪ 𝐴 ) ) )
46	45	alrimdv	⊢ ( 𝐴 ⊆ P → ( 𝑥 ∈ ∪ 𝐴 → ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ ∪ 𝐴 ) ) )
47		eluni	⊢ ( 𝑥 ∈ ∪ 𝐴 ↔ ∃ 𝑧 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴 ) )
48		prnmax	⊢ ( ( 𝑧 ∈ P ∧ 𝑥 ∈ 𝑧 ) → ∃ 𝑦 ∈ 𝑧 𝑥 <Q 𝑦 )
49	48	ex	⊢ ( 𝑧 ∈ P → ( 𝑥 ∈ 𝑧 → ∃ 𝑦 ∈ 𝑧 𝑥 <Q 𝑦 ) )
50	10 49	syl6	⊢ ( 𝐴 ⊆ P → ( 𝑧 ∈ 𝐴 → ( 𝑥 ∈ 𝑧 → ∃ 𝑦 ∈ 𝑧 𝑥 <Q 𝑦 ) ) )
51	50	com23	⊢ ( 𝐴 ⊆ P → ( 𝑥 ∈ 𝑧 → ( 𝑧 ∈ 𝐴 → ∃ 𝑦 ∈ 𝑧 𝑥 <Q 𝑦 ) ) )
52	51	imp	⊢ ( ( 𝐴 ⊆ P ∧ 𝑥 ∈ 𝑧 ) → ( 𝑧 ∈ 𝐴 → ∃ 𝑦 ∈ 𝑧 𝑥 <Q 𝑦 ) )
53		ssrexv	⊢ ( 𝑧 ⊆ ∪ 𝐴 → ( ∃ 𝑦 ∈ 𝑧 𝑥 <Q 𝑦 → ∃ 𝑦 ∈ ∪ 𝐴 𝑥 <Q 𝑦 ) )
54	14 53	syl	⊢ ( 𝑧 ∈ 𝐴 → ( ∃ 𝑦 ∈ 𝑧 𝑥 <Q 𝑦 → ∃ 𝑦 ∈ ∪ 𝐴 𝑥 <Q 𝑦 ) )
55	52 54	sylcom	⊢ ( ( 𝐴 ⊆ P ∧ 𝑥 ∈ 𝑧 ) → ( 𝑧 ∈ 𝐴 → ∃ 𝑦 ∈ ∪ 𝐴 𝑥 <Q 𝑦 ) )
56	55	expimpd	⊢ ( 𝐴 ⊆ P → ( ( 𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴 ) → ∃ 𝑦 ∈ ∪ 𝐴 𝑥 <Q 𝑦 ) )
57	56	exlimdv	⊢ ( 𝐴 ⊆ P → ( ∃ 𝑧 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴 ) → ∃ 𝑦 ∈ ∪ 𝐴 𝑥 <Q 𝑦 ) )
58	47 57	syl5bi	⊢ ( 𝐴 ⊆ P → ( 𝑥 ∈ ∪ 𝐴 → ∃ 𝑦 ∈ ∪ 𝐴 𝑥 <Q 𝑦 ) )
59	46 58	jcad	⊢ ( 𝐴 ⊆ P → ( 𝑥 ∈ ∪ 𝐴 → ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ ∪ 𝐴 ) ∧ ∃ 𝑦 ∈ ∪ 𝐴 𝑥 <Q 𝑦 ) ) )
60	59	ralrimiv	⊢ ( 𝐴 ⊆ P → ∀ 𝑥 ∈ ∪ 𝐴 ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ ∪ 𝐴 ) ∧ ∃ 𝑦 ∈ ∪ 𝐴 𝑥 <Q 𝑦 ) )
61	8 60	syl	⊢ ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ P ∀ 𝑦 ∈ 𝐴 𝑦 <P 𝑥 ) → ∀ 𝑥 ∈ ∪ 𝐴 ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ ∪ 𝐴 ) ∧ ∃ 𝑦 ∈ ∪ 𝐴 𝑥 <Q 𝑦 ) )
62		elnp	⊢ ( ∪ 𝐴 ∈ P ↔ ( ( ∅ ⊊ ∪ 𝐴 ∧ ∪ 𝐴 ⊊ Q ) ∧ ∀ 𝑥 ∈ ∪ 𝐴 ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ ∪ 𝐴 ) ∧ ∃ 𝑦 ∈ ∪ 𝐴 𝑥 <Q 𝑦 ) ) )
63	35 61 62	sylanbrc	⊢ ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ P ∀ 𝑦 ∈ 𝐴 𝑦 <P 𝑥 ) → ∪ 𝐴 ∈ P )