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

Metamath Proof Explorer

Theorem 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 ( 𝐴 ⊆ P → ( ( 𝑦 ∈ 𝐴 → ¬ ∪ 𝐴 <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 ralnex ⊢ ( ∀ 𝑧 ∈ 𝐴 ¬ 𝑦 <P 𝑧 ↔ ¬ ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 )
5 ssel2 ⊢ ( ( 𝐴 ⊆ P ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ P )
6 ltsopr ⊢ <P Or P
7 sotric ⊢ ( ( <P Or P ∧ ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ) → ( 𝑦 <P 𝑧 ↔ ¬ ( 𝑦 = 𝑧 ∨ 𝑧 <P 𝑦 ) ) )
8 6 7 mpan ⊢ ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) → ( 𝑦 <P 𝑧 ↔ ¬ ( 𝑦 = 𝑧 ∨ 𝑧 <P 𝑦 ) ) )
9 8 con2bid ⊢ ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) → ( ( 𝑦 = 𝑧 ∨ 𝑧 <P 𝑦 ) ↔ ¬ 𝑦 <P 𝑧 ) )
10 9 ancoms ⊢ ( ( 𝑧 ∈ P ∧ 𝑦 ∈ P ) → ( ( 𝑦 = 𝑧 ∨ 𝑧 <P 𝑦 ) ↔ ¬ 𝑦 <P 𝑧 ) )
11 ltprord ⊢ ( ( 𝑧 ∈ P ∧ 𝑦 ∈ P ) → ( 𝑧 <P 𝑦 ↔ 𝑧 ⊊ 𝑦 ) )
12 11 orbi2d ⊢ ( ( 𝑧 ∈ P ∧ 𝑦 ∈ P ) → ( ( 𝑦 = 𝑧 ∨ 𝑧 <P 𝑦 ) ↔ ( 𝑦 = 𝑧 ∨ 𝑧 ⊊ 𝑦 ) ) )
13 sspss ⊢ ( 𝑧 ⊆ 𝑦 ↔ ( 𝑧 ⊊ 𝑦 ∨ 𝑧 = 𝑦 ) )
14 equcom ⊢ ( 𝑧 = 𝑦 ↔ 𝑦 = 𝑧 )
15 14 orbi2i ⊢ ( ( 𝑧 ⊊ 𝑦 ∨ 𝑧 = 𝑦 ) ↔ ( 𝑧 ⊊ 𝑦 ∨ 𝑦 = 𝑧 ) )
16 orcom ⊢ ( ( 𝑧 ⊊ 𝑦 ∨ 𝑦 = 𝑧 ) ↔ ( 𝑦 = 𝑧 ∨ 𝑧 ⊊ 𝑦 ) )
17 13 15 16 3bitri ⊢ ( 𝑧 ⊆ 𝑦 ↔ ( 𝑦 = 𝑧 ∨ 𝑧 ⊊ 𝑦 ) )
18 12 17 bitr4di ⊢ ( ( 𝑧 ∈ P ∧ 𝑦 ∈ P ) → ( ( 𝑦 = 𝑧 ∨ 𝑧 <P 𝑦 ) ↔ 𝑧 ⊆ 𝑦 ) )
19 10 18 bitr3d ⊢ ( ( 𝑧 ∈ P ∧ 𝑦 ∈ P ) → ( ¬ 𝑦 <P 𝑧 ↔ 𝑧 ⊆ 𝑦 ) )
20 5 19 sylan ⊢ ( ( ( 𝐴 ⊆ P ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ∈ P ) → ( ¬ 𝑦 <P 𝑧 ↔ 𝑧 ⊆ 𝑦 ) )
21 20 an32s ⊢ ( ( ( 𝐴 ⊆ P ∧ 𝑦 ∈ P ) ∧ 𝑧 ∈ 𝐴 ) → ( ¬ 𝑦 <P 𝑧 ↔ 𝑧 ⊆ 𝑦 ) )
22 21 ralbidva ⊢ ( ( 𝐴 ⊆ P ∧ 𝑦 ∈ P ) → ( ∀ 𝑧 ∈ 𝐴 ¬ 𝑦 <P 𝑧 ↔ ∀ 𝑧 ∈ 𝐴 𝑧 ⊆ 𝑦 ) )
23 4 22 bitr3id ⊢ ( ( 𝐴 ⊆ P ∧ 𝑦 ∈ P ) → ( ¬ ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 ↔ ∀ 𝑧 ∈ 𝐴 𝑧 ⊆ 𝑦 ) )
24 unissb ⊢ ( ∪ 𝐴 ⊆ 𝑦 ↔ ∀ 𝑧 ∈ 𝐴 𝑧 ⊆ 𝑦 )
25 23 24 bitr4di ⊢ ( ( 𝐴 ⊆ P ∧ 𝑦 ∈ P ) → ( ¬ ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 ↔ ∪ 𝐴 ⊆ 𝑦 ) )
26 ssnpss ⊢ ( ∪ 𝐴 ⊆ 𝑦 → ¬ 𝑦 ⊊ ∪ 𝐴 )
27 ltprord ⊢ ( ( 𝑦 ∈ P ∧ ∪ 𝐴 ∈ P ) → ( 𝑦 <P ∪ 𝐴 ↔ 𝑦 ⊊ ∪ 𝐴 ) )
28 27 biimpd ⊢ ( ( 𝑦 ∈ P ∧ ∪ 𝐴 ∈ P ) → ( 𝑦 <P ∪ 𝐴 → 𝑦 ⊊ ∪ 𝐴 ) )
29 2 28 mpcom ⊢ ( 𝑦 <P ∪ 𝐴 → 𝑦 ⊊ ∪ 𝐴 )
30 26 29 nsyl ⊢ ( ∪ 𝐴 ⊆ 𝑦 → ¬ 𝑦 <P ∪ 𝐴 )
31 25 30 biimtrdi ⊢ ( ( 𝐴 ⊆ P ∧ 𝑦 ∈ P ) → ( ¬ ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 → ¬ 𝑦 <P ∪ 𝐴 ) )
32 31 con4d ⊢ ( ( 𝐴 ⊆ P ∧ 𝑦 ∈ P ) → ( 𝑦 <P ∪ 𝐴 → ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 ) )
33 32 ex ⊢ ( 𝐴 ⊆ P → ( 𝑦 ∈ P → ( 𝑦 <P ∪ 𝐴 → ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 ) ) )
34 3 33 syl5 ⊢ ( 𝐴 ⊆ P → ( 𝑦 <P ∪ 𝐴 → ( 𝑦 <P ∪ 𝐴 → ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 ) ) )
35 34 pm2.43d ⊢ ( 𝐴 ⊆ P → ( 𝑦 <P ∪ 𝐴 → ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 ) )
36 elssuni ⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ⊆ ∪ 𝐴 )
37 ssnpss ⊢ ( 𝑦 ⊆ ∪ 𝐴 → ¬ ∪ 𝐴 ⊊ 𝑦 )
38 36 37 syl ⊢ ( 𝑦 ∈ 𝐴 → ¬ ∪ 𝐴 ⊊ 𝑦 )
39 1 brel ⊢ ( ∪ 𝐴 <P 𝑦 → ( ∪ 𝐴 ∈ P ∧ 𝑦 ∈ P ) )
40 ltprord ⊢ ( ( ∪ 𝐴 ∈ P ∧ 𝑦 ∈ P ) → ( ∪ 𝐴 <P 𝑦 ↔ ∪ 𝐴 ⊊ 𝑦 ) )
41 40 biimpd ⊢ ( ( ∪ 𝐴 ∈ P ∧ 𝑦 ∈ P ) → ( ∪ 𝐴 <P 𝑦 → ∪ 𝐴 ⊊ 𝑦 ) )
42 39 41 mpcom ⊢ ( ∪ 𝐴 <P 𝑦 → ∪ 𝐴 ⊊ 𝑦 )
43 38 42 nsyl ⊢ ( 𝑦 ∈ 𝐴 → ¬ ∪ 𝐴 <P 𝑦 )
44 35 43 jctil ⊢ ( 𝐴 ⊆ P → ( ( 𝑦 ∈ 𝐴 → ¬ ∪ 𝐴 <P 𝑦 ) ∧ ( 𝑦 <P ∪ 𝐴 → ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 ) ) )