Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  supexpr Structured version   Visualization version   GIF version

Theorem supexpr 9755
 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.)
Assertion
Ref Expression
supexpr ((𝐴 ≠ ∅ ∧ ∃𝑥P𝑦𝐴 𝑦<P 𝑥) → ∃𝑥P (∀𝑦𝐴 ¬ 𝑥<P 𝑦 ∧ ∀𝑦P (𝑦<P 𝑥 → ∃𝑧𝐴 𝑦<P 𝑧)))
Distinct variable group:   𝑥,𝑦,𝑧,𝐴

Proof of Theorem supexpr
StepHypRef Expression
1 suplem1pr 9753 . 2 ((𝐴 ≠ ∅ ∧ ∃𝑥P𝑦𝐴 𝑦<P 𝑥) → 𝐴P)
2 ltrelpr 9699 . . . . . . . . 9 <P ⊆ (P × P)
32brel 5090 . . . . . . . 8 (𝑦<P 𝑥 → (𝑦P𝑥P))
43simpld 474 . . . . . . 7 (𝑦<P 𝑥𝑦P)
54ralimi 2936 . . . . . 6 (∀𝑦𝐴 𝑦<P 𝑥 → ∀𝑦𝐴 𝑦P)
6 dfss3 3558 . . . . . 6 (𝐴P ↔ ∀𝑦𝐴 𝑦P)
75, 6sylibr 223 . . . . 5 (∀𝑦𝐴 𝑦<P 𝑥𝐴P)
87rexlimivw 3011 . . . 4 (∃𝑥P𝑦𝐴 𝑦<P 𝑥𝐴P)
98adantl 481 . . 3 ((𝐴 ≠ ∅ ∧ ∃𝑥P𝑦𝐴 𝑦<P 𝑥) → 𝐴P)
10 suplem2pr 9754 . . . . . 6 (𝐴P → ((𝑦𝐴 → ¬ 𝐴<P 𝑦) ∧ (𝑦<P 𝐴 → ∃𝑧𝐴 𝑦<P 𝑧)))
1110simpld 474 . . . . 5 (𝐴P → (𝑦𝐴 → ¬ 𝐴<P 𝑦))
1211ralrimiv 2948 . . . 4 (𝐴P → ∀𝑦𝐴 ¬ 𝐴<P 𝑦)
1310simprd 478 . . . . 5 (𝐴P → (𝑦<P 𝐴 → ∃𝑧𝐴 𝑦<P 𝑧))
1413ralrimivw 2950 . . . 4 (𝐴P → ∀𝑦P (𝑦<P 𝐴 → ∃𝑧𝐴 𝑦<P 𝑧))
1512, 14jca 553 . . 3 (𝐴P → (∀𝑦𝐴 ¬ 𝐴<P 𝑦 ∧ ∀𝑦P (𝑦<P 𝐴 → ∃𝑧𝐴 𝑦<P 𝑧)))
169, 15syl 17 . 2 ((𝐴 ≠ ∅ ∧ ∃𝑥P𝑦𝐴 𝑦<P 𝑥) → (∀𝑦𝐴 ¬ 𝐴<P 𝑦 ∧ ∀𝑦P (𝑦<P 𝐴 → ∃𝑧𝐴 𝑦<P 𝑧)))
17 breq1 4586 . . . . . 6 (𝑥 = 𝐴 → (𝑥<P 𝑦 𝐴<P 𝑦))
1817notbid 307 . . . . 5 (𝑥 = 𝐴 → (¬ 𝑥<P 𝑦 ↔ ¬ 𝐴<P 𝑦))
1918ralbidv 2969 . . . 4 (𝑥 = 𝐴 → (∀𝑦𝐴 ¬ 𝑥<P 𝑦 ↔ ∀𝑦𝐴 ¬ 𝐴<P 𝑦))
20 breq2 4587 . . . . . 6 (𝑥 = 𝐴 → (𝑦<P 𝑥𝑦<P 𝐴))
2120imbi1d 330 . . . . 5 (𝑥 = 𝐴 → ((𝑦<P 𝑥 → ∃𝑧𝐴 𝑦<P 𝑧) ↔ (𝑦<P 𝐴 → ∃𝑧𝐴 𝑦<P 𝑧)))
2221ralbidv 2969 . . . 4 (𝑥 = 𝐴 → (∀𝑦P (𝑦<P 𝑥 → ∃𝑧𝐴 𝑦<P 𝑧) ↔ ∀𝑦P (𝑦<P 𝐴 → ∃𝑧𝐴 𝑦<P 𝑧)))
2319, 22anbi12d 743 . . 3 (𝑥 = 𝐴 → ((∀𝑦𝐴 ¬ 𝑥<P 𝑦 ∧ ∀𝑦P (𝑦<P 𝑥 → ∃𝑧𝐴 𝑦<P 𝑧)) ↔ (∀𝑦𝐴 ¬ 𝐴<P 𝑦 ∧ ∀𝑦P (𝑦<P 𝐴 → ∃𝑧𝐴 𝑦<P 𝑧))))
2423rspcev 3282 . 2 (( 𝐴P ∧ (∀𝑦𝐴 ¬ 𝐴<P 𝑦 ∧ ∀𝑦P (𝑦<P 𝐴 → ∃𝑧𝐴 𝑦<P 𝑧))) → ∃𝑥P (∀𝑦𝐴 ¬ 𝑥<P 𝑦 ∧ ∀𝑦P (𝑦<P 𝑥 → ∃𝑧𝐴 𝑦<P 𝑧)))
251, 16, 24syl2anc 691 1 ((𝐴 ≠ ∅ ∧ ∃𝑥P𝑦𝐴 𝑦<P 𝑥) → ∃𝑥P (∀𝑦𝐴 ¬ 𝑥<P 𝑦 ∧ ∀𝑦P (𝑦<P 𝑥 → ∃𝑧𝐴 𝑦<P 𝑧)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897   ⊆ wss 3540  ∅c0 3874  ∪ cuni 4372   class class class wbr 4583  Pcnp 9560
 Copyright terms: Public domain W3C validator