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

 Description: A positive real has no largest member. Addition version. (Contributed by NM, 7-Apr-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.)
Assertion
Ref Expression
prnmadd ((𝐴P𝐵𝐴) → ∃𝑥(𝐵 +Q 𝑥) ∈ 𝐴)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 prnmax 9761 . 2 ((𝐴P𝐵𝐴) → ∃𝑦𝐴 𝐵 <Q 𝑦)
2 ltrelnq 9692 . . . . . . 7 <Q ⊆ (Q × Q)
32brel 5128 . . . . . 6 (𝐵 <Q 𝑦 → (𝐵Q𝑦Q))
43simprd 479 . . . . 5 (𝐵 <Q 𝑦𝑦Q)
5 ltexnq 9741 . . . . . 6 (𝑦Q → (𝐵 <Q 𝑦 ↔ ∃𝑥(𝐵 +Q 𝑥) = 𝑦))
65biimpcd 239 . . . . 5 (𝐵 <Q 𝑦 → (𝑦Q → ∃𝑥(𝐵 +Q 𝑥) = 𝑦))
74, 6mpd 15 . . . 4 (𝐵 <Q 𝑦 → ∃𝑥(𝐵 +Q 𝑥) = 𝑦)
8 eleq1a 2693 . . . . 5 (𝑦𝐴 → ((𝐵 +Q 𝑥) = 𝑦 → (𝐵 +Q 𝑥) ∈ 𝐴))
98eximdv 1843 . . . 4 (𝑦𝐴 → (∃𝑥(𝐵 +Q 𝑥) = 𝑦 → ∃𝑥(𝐵 +Q 𝑥) ∈ 𝐴))
107, 9syl5 34 . . 3 (𝑦𝐴 → (𝐵 <Q 𝑦 → ∃𝑥(𝐵 +Q 𝑥) ∈ 𝐴))
1110rexlimiv 3020 . 2 (∃𝑦𝐴 𝐵 <Q 𝑦 → ∃𝑥(𝐵 +Q 𝑥) ∈ 𝐴)
121, 11syl 17 1 ((𝐴P𝐵𝐴) → ∃𝑥(𝐵 +Q 𝑥) ∈ 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   = wceq 1480  ∃wex 1701   ∈ wcel 1987  ∃wrex 2908   class class class wbr 4613  (class class class)co 6604  Qcnq 9618   +Q cplq 9621
 Copyright terms: Public domain W3C validator