This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrid ⊢ ( 𝐴 ⊆ P → ( 𝐴 ≠ ∅ → ∅ ⊊ ∪ 𝐴 ) )
21 prpssnq ⊢ ( 𝑥 ∈ P → 𝑥 ⊊ Q )
22 21 adantl ⊢ ( ( 𝐴 ⊆ P ∧ 𝑥 ∈ P ) → 𝑥 ⊊ Q )
23 ltprord ⊢ ( ( 𝑦 ∈ P ∧ 𝑥 ∈ P ) → ( 𝑦 <P 𝑥 ↔ 𝑦 ⊊ 𝑥 ) )
24 pssss ⊢ ( 𝑦 ⊊ 𝑥 → 𝑦 ⊆ 𝑥 )
25 23 24 biimtrdi ⊢ ( ( 𝑦 ∈ 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 biimtrid ⊢ ( 𝐴 ⊆ 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 )