Metamath Proof Explorer

Theorem supexpr

Description: The union of a nonempty, bounded set of positive reals has a supremum. Part of Proposition 9-3.3 of Gleason p. 122. (Contributed by NM, 19-May-1996) (New usage is discouraged.)

Ref Expression
Assertion supexpr ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ P ∀ 𝑦 ∈ 𝐴 𝑦 <P 𝑥 ) → ∃ 𝑥 ∈ P ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <P 𝑦 ∧ ∀ 𝑦 ∈ P ( 𝑦 <P 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 suplem1pr ⊢ ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ P ∀ 𝑦 ∈ 𝐴 𝑦 <P 𝑥 ) → ∪ 𝐴 ∈ P )
2 ltrelpr ⊢ <P ⊆ ( P × P )
3 2 brel ⊢ ( 𝑦 <P 𝑥 → ( 𝑦 ∈ P ∧ 𝑥 ∈ P ) )
4 3 simpld ⊢ ( 𝑦 <P 𝑥 → 𝑦 ∈ P )
5 4 ralimi ⊢ ( ∀ 𝑦 ∈ 𝐴 𝑦 <P 𝑥 → ∀ 𝑦 ∈ 𝐴 𝑦 ∈ P )
6 dfss3 ⊢ ( 𝐴 ⊆ P ↔ ∀ 𝑦 ∈ 𝐴 𝑦 ∈ P )
7 5 6 sylibr ⊢ ( ∀ 𝑦 ∈ 𝐴 𝑦 <P 𝑥 → 𝐴 ⊆ P )
8 7 rexlimivw ⊢ ( ∃ 𝑥 ∈ P ∀ 𝑦 ∈ 𝐴 𝑦 <P 𝑥 → 𝐴 ⊆ P )
9 8 adantl ⊢ ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ P ∀ 𝑦 ∈ 𝐴 𝑦 <P 𝑥 ) → 𝐴 ⊆ P )
10 suplem2pr ⊢ ( 𝐴 ⊆ P → ( ( 𝑦 ∈ 𝐴 → ¬ ∪ 𝐴 <P 𝑦 ) ∧ ( 𝑦 <P ∪ 𝐴 → ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 ) ) )
11 10 simpld ⊢ ( 𝐴 ⊆ P → ( 𝑦 ∈ 𝐴 → ¬ ∪ 𝐴 <P 𝑦 ) )
12 11 ralrimiv ⊢ ( 𝐴 ⊆ P → ∀ 𝑦 ∈ 𝐴 ¬ ∪ 𝐴 <P 𝑦 )
13 10 simprd ⊢ ( 𝐴 ⊆ P → ( 𝑦 <P ∪ 𝐴 → ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 ) )
14 13 ralrimivw ⊢ ( 𝐴 ⊆ P → ∀ 𝑦 ∈ P ( 𝑦 <P ∪ 𝐴 → ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 ) )
15 12 14 jca ⊢ ( 𝐴 ⊆ P → ( ∀ 𝑦 ∈ 𝐴 ¬ ∪ 𝐴 <P 𝑦 ∧ ∀ 𝑦 ∈ P ( 𝑦 <P ∪ 𝐴 → ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 ) ) )
16 9 15 syl ⊢ ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ P ∀ 𝑦 ∈ 𝐴 𝑦 <P 𝑥 ) → ( ∀ 𝑦 ∈ 𝐴 ¬ ∪ 𝐴 <P 𝑦 ∧ ∀ 𝑦 ∈ P ( 𝑦 <P ∪ 𝐴 → ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 ) ) )
17 breq1 ⊢ ( 𝑥 = ∪ 𝐴 → ( 𝑥 <P 𝑦 ↔ ∪ 𝐴 <P 𝑦 ) )
18 17 notbid ⊢ ( 𝑥 = ∪ 𝐴 → ( ¬ 𝑥 <P 𝑦 ↔ ¬ ∪ 𝐴 <P 𝑦 ) )
19 18 ralbidv ⊢ ( 𝑥 = ∪ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <P 𝑦 ↔ ∀ 𝑦 ∈ 𝐴 ¬ ∪ 𝐴 <P 𝑦 ) )
20 breq2 ⊢ ( 𝑥 = ∪ 𝐴 → ( 𝑦 <P 𝑥 ↔ 𝑦 <P ∪ 𝐴 ) )
21 20 imbi1d ⊢ ( 𝑥 = ∪ 𝐴 → ( ( 𝑦 <P 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 ) ↔ ( 𝑦 <P ∪ 𝐴 → ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 ) ) )
22 21 ralbidv ⊢ ( 𝑥 = ∪ 𝐴 → ( ∀ 𝑦 ∈ P ( 𝑦 <P 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 ) ↔ ∀ 𝑦 ∈ P ( 𝑦 <P ∪ 𝐴 → ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 ) ) )
23 19 22 anbi12d ⊢ ( 𝑥 = ∪ 𝐴 → ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <P 𝑦 ∧ ∀ 𝑦 ∈ P ( 𝑦 <P 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝐴 ¬ ∪ 𝐴 <P 𝑦 ∧ ∀ 𝑦 ∈ P ( 𝑦 <P ∪ 𝐴 → ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 ) ) ) )
24 23 rspcev ⊢ ( ( ∪ 𝐴 ∈ P ∧ ( ∀ 𝑦 ∈ 𝐴 ¬ ∪ 𝐴 <P 𝑦 ∧ ∀ 𝑦 ∈ P ( 𝑦 <P ∪ 𝐴 → ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 ) ) ) → ∃ 𝑥 ∈ P ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <P 𝑦 ∧ ∀ 𝑦 ∈ P ( 𝑦 <P 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 ) ) )
25 1 16 24 syl2anc ⊢ ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ P ∀ 𝑦 ∈ 𝐴 𝑦 <P 𝑥 ) → ∃ 𝑥 ∈ P ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <P 𝑦 ∧ ∀ 𝑦 ∈ P ( 𝑦 <P 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 ) ) )