Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  prnmaddl Structured version   GIF version

Theorem prnmaddl 6344
 Description: A lower cut has no largest member. Addition version. (Contributed by Jim Kingdon, 29-Sep-2019.)
Assertion
Ref Expression
prnmaddl ((⟨𝐿, 𝑈 P B 𝐿) → x Q (B +Q x) 𝐿)
Distinct variable groups:   x,B   x,𝐿   x,𝑈

Proof of Theorem prnmaddl
Dummy variable y is distinct from all other variables.
StepHypRef Expression
1 prnmaxl 6342 . 2 ((⟨𝐿, 𝑈 P B 𝐿) → y 𝐿 B <Q y)
2 ltrelnq 6224 . . . . . 6 <Q ⊆ (Q × Q)
32brel 4319 . . . . 5 (B <Q y → (B Q y Q))
4 ltexnqq 6266 . . . . . 6 ((B Q y Q) → (B <Q yx Q (B +Q x) = y))
54biimpcd 148 . . . . 5 (B <Q y → ((B Q y Q) → x Q (B +Q x) = y))
63, 5mpd 13 . . . 4 (B <Q yx Q (B +Q x) = y)
7 eleq1a 2091 . . . . 5 (y 𝐿 → ((B +Q x) = y → (B +Q x) 𝐿))
87reximdv 2398 . . . 4 (y 𝐿 → (x Q (B +Q x) = yx Q (B +Q x) 𝐿))
96, 8syl5 28 . . 3 (y 𝐿 → (B <Q yx Q (B +Q x) 𝐿))
109rexlimiv 2405 . 2 (y 𝐿 B <Q yx Q (B +Q x) 𝐿)
111, 10syl 14 1 ((⟨𝐿, 𝑈 P B 𝐿) → x Q (B +Q x) 𝐿)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   = wceq 1228   ∈ wcel 1374  ∃wrex 2285  ⟨cop 3353   class class class wbr 3738  (class class class)co 5436  Qcnq 6138   +Q cplq 6140
 Copyright terms: Public domain W3C validator