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

 Description: Lemma for addnqpr1 6541. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 28-Apr-2020.)
Assertion
Ref Expression
addnqpr1lemiu (A Q → (2nd ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩) ⊆ (2nd ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P)))
Distinct variable group:   A,𝑙,u

Proof of Theorem addnqpr1lemiu
Dummy variable 𝑟 is distinct from all other variables.
StepHypRef Expression
1 addnqpr1lemrl 6537 . . . . . 6 (A Q → (1st ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P)) ⊆ (1st ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩))
2 ltsonq 6382 . . . . . . . . 9 <Q Or Q
3 1nq 6350 . . . . . . . . . 10 1Q Q
4 addclnq 6359 . . . . . . . . . 10 ((A Q 1Q Q) → (A +Q 1Q) Q)
53, 4mpan2 401 . . . . . . . . 9 (A Q → (A +Q 1Q) Q)
6 sonr 4045 . . . . . . . . 9 (( <Q Or Q (A +Q 1Q) Q) → ¬ (A +Q 1Q) <Q (A +Q 1Q))
72, 5, 6sylancr 393 . . . . . . . 8 (A Q → ¬ (A +Q 1Q) <Q (A +Q 1Q))
8 ltrelnq 6349 . . . . . . . . . . . 12 <Q ⊆ (Q × Q)
98brel 4335 . . . . . . . . . . 11 ((A +Q 1Q) <Q (A +Q 1Q) → ((A +Q 1Q) Q (A +Q 1Q) Q))
109simpld 105 . . . . . . . . . 10 ((A +Q 1Q) <Q (A +Q 1Q) → (A +Q 1Q) Q)
11 elex 2560 . . . . . . . . . 10 ((A +Q 1Q) Q → (A +Q 1Q) V)
1210, 11syl 14 . . . . . . . . 9 ((A +Q 1Q) <Q (A +Q 1Q) → (A +Q 1Q) V)
13 breq1 3758 . . . . . . . . 9 (𝑙 = (A +Q 1Q) → (𝑙 <Q (A +Q 1Q) ↔ (A +Q 1Q) <Q (A +Q 1Q)))
1412, 13elab3 2688 . . . . . . . 8 ((A +Q 1Q) {𝑙𝑙 <Q (A +Q 1Q)} ↔ (A +Q 1Q) <Q (A +Q 1Q))
157, 14sylnibr 601 . . . . . . 7 (A Q → ¬ (A +Q 1Q) {𝑙𝑙 <Q (A +Q 1Q)})
16 ltnqex 6531 . . . . . . . . 9 {𝑙𝑙 <Q (A +Q 1Q)} V
17 gtnqex 6532 . . . . . . . . 9 {u ∣ (A +Q 1Q) <Q u} V
1816, 17op1st 5715 . . . . . . . 8 (1st ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩) = {𝑙𝑙 <Q (A +Q 1Q)}
1918eleq2i 2101 . . . . . . 7 ((A +Q 1Q) (1st ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩) ↔ (A +Q 1Q) {𝑙𝑙 <Q (A +Q 1Q)})
2015, 19sylnibr 601 . . . . . 6 (A Q → ¬ (A +Q 1Q) (1st ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩))
211, 20ssneldd 2942 . . . . 5 (A Q → ¬ (A +Q 1Q) (1st ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P)))
2221adantr 261 . . . 4 ((A Q 𝑟 (2nd ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩)) → ¬ (A +Q 1Q) (1st ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P)))
23 nqprlu 6530 . . . . . . . . 9 (A Q → ⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ P)
2423adantr 261 . . . . . . . 8 ((A Q 𝑟 (2nd ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩)) → ⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ P)
25 1pr 6534 . . . . . . . 8 1P P
26 addclpr 6520 . . . . . . . 8 ((⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ P 1P P) → (⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P) P)
2724, 25, 26sylancl 392 . . . . . . 7 ((A Q 𝑟 (2nd ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩)) → (⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P) P)
28 prop 6457 . . . . . . 7 ((⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P) P → ⟨(1st ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P)), (2nd ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P))⟩ P)
2927, 28syl 14 . . . . . 6 ((A Q 𝑟 (2nd ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩)) → ⟨(1st ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P)), (2nd ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P))⟩ P)
30 vex 2554 . . . . . . . . 9 𝑟 V
31 breq2 3759 . . . . . . . . 9 (u = 𝑟 → ((A +Q 1Q) <Q u ↔ (A +Q 1Q) <Q 𝑟))
3216, 17op2nd 5716 . . . . . . . . 9 (2nd ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩) = {u ∣ (A +Q 1Q) <Q u}
3330, 31, 32elab2 2684 . . . . . . . 8 (𝑟 (2nd ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩) ↔ (A +Q 1Q) <Q 𝑟)
3433biimpi 113 . . . . . . 7 (𝑟 (2nd ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩) → (A +Q 1Q) <Q 𝑟)
3534adantl 262 . . . . . 6 ((A Q 𝑟 (2nd ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩)) → (A +Q 1Q) <Q 𝑟)
36 prloc 6473 . . . . . 6 ((⟨(1st ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P)), (2nd ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P))⟩ P (A +Q 1Q) <Q 𝑟) → ((A +Q 1Q) (1st ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P)) 𝑟 (2nd ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P))))
3729, 35, 36syl2anc 391 . . . . 5 ((A Q 𝑟 (2nd ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩)) → ((A +Q 1Q) (1st ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P)) 𝑟 (2nd ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P))))
3837orcomd 647 . . . 4 ((A Q 𝑟 (2nd ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩)) → (𝑟 (2nd ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P)) (A +Q 1Q) (1st ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P))))
3922, 38ecased 1238 . . 3 ((A Q 𝑟 (2nd ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩)) → 𝑟 (2nd ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P)))
4039ex 108 . 2 (A Q → (𝑟 (2nd ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩) → 𝑟 (2nd ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P))))
4140ssrdv 2945 1 (A Q → (2nd ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩) ⊆ (2nd ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P)))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ∨ wo 628   ∈ wcel 1390  {cab 2023  Vcvv 2551   ⊆ wss 2911  ⟨cop 3370   class class class wbr 3755   Or wor 4023  ‘cfv 4845  (class class class)co 5455  1st c1st 5707  2nd c2nd 5708  Qcnq 6264  1Qc1q 6265   +Q cplq 6266
 Copyright terms: Public domain W3C validator