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

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

Dummy variable 𝑟 is distinct from all other variables.
StepHypRef Expression
1 addnqpr1lemru 6538 . . . . . 6 (A Q → (2nd ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P)) ⊆ (2nd ‘⟨{𝑙𝑙 <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 breq2 3759 . . . . . . . . 9 (u = (A +Q 1Q) → ((A +Q 1Q) <Q u ↔ (A +Q 1Q) <Q (A +Q 1Q)))
1412, 13elab3 2688 . . . . . . . 8 ((A +Q 1Q) {u ∣ (A +Q 1Q) <Q u} ↔ (A +Q 1Q) <Q (A +Q 1Q))
157, 14sylnibr 601 . . . . . . 7 (A Q → ¬ (A +Q 1Q) {u ∣ (A +Q 1Q) <Q u})
16 ltnqex 6531 . . . . . . . . 9 {𝑙𝑙 <Q (A +Q 1Q)} V
17 gtnqex 6532 . . . . . . . . 9 {u ∣ (A +Q 1Q) <Q u} V
1816, 17op2nd 5716 . . . . . . . 8 (2nd ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩) = {u ∣ (A +Q 1Q) <Q u}
1918eleq2i 2101 . . . . . . 7 ((A +Q 1Q) (2nd ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩) ↔ (A +Q 1Q) {u ∣ (A +Q 1Q) <Q u})
2015, 19sylnibr 601 . . . . . 6 (A Q → ¬ (A +Q 1Q) (2nd ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩))
211, 20ssneldd 2942 . . . . 5 (A Q → ¬ (A +Q 1Q) (2nd ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P)))
2221adantr 261 . . . 4 ((A Q 𝑟 (1st ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩)) → ¬ (A +Q 1Q) (2nd ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P)))
23 nqprlu 6530 . . . . . . . 8 (A Q → ⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ P)
2423adantr 261 . . . . . . 7 ((A Q 𝑟 (1st ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩)) → ⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ P)
25 1pr 6534 . . . . . . 7 1P P
26 addclpr 6520 . . . . . . 7 ((⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ P 1P P) → (⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P) P)
2724, 25, 26sylancl 392 . . . . . 6 ((A Q 𝑟 (1st ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩)) → (⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P) P)
28 prop 6457 . . . . . 6 ((⟨{𝑙𝑙 <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 . . . . 5 ((A Q 𝑟 (1st ‘⟨{𝑙𝑙 <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 . . . . . . . 8 𝑟 V
31 breq1 3758 . . . . . . . 8 (𝑙 = 𝑟 → (𝑙 <Q (A +Q 1Q) ↔ 𝑟 <Q (A +Q 1Q)))
3216, 17op1st 5715 . . . . . . . 8 (1st ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩) = {𝑙𝑙 <Q (A +Q 1Q)}
3330, 31, 32elab2 2684 . . . . . . 7 (𝑟 (1st ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩) ↔ 𝑟 <Q (A +Q 1Q))
3433biimpi 113 . . . . . 6 (𝑟 (1st ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩) → 𝑟 <Q (A +Q 1Q))
3534adantl 262 . . . . 5 ((A Q 𝑟 (1st ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩)) → 𝑟 <Q (A +Q 1Q))
36 prloc 6473 . . . . 5 ((⟨(1st ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P)), (2nd ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P))⟩ P 𝑟 <Q (A +Q 1Q)) → (𝑟 (1st ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P)) (A +Q 1Q) (2nd ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P))))
3729, 35, 36syl2anc 391 . . . 4 ((A Q 𝑟 (1st ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩)) → (𝑟 (1st ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P)) (A +Q 1Q) (2nd ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P))))
3822, 37ecased 1238 . . 3 ((A Q 𝑟 (1st ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩)) → 𝑟 (1st ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P)))
3938ex 108 . 2 (A Q → (𝑟 (1st ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩) → 𝑟 (1st ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P))))
4039ssrdv 2945 1 (A Q → (1st ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩) ⊆ (1st ‘(⟨{𝑙𝑙 <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