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

Theorem genpcuu 6824
 Description: Upward closure of an operation on positive reals. (Contributed by Jim Kingdon, 8-Nov-2019.)
Hypotheses
Ref Expression
genpelvl.1 𝐹 = (𝑤P, 𝑣P ↦ ⟨{𝑥Q ∣ ∃𝑦Q𝑧Q (𝑦 ∈ (1st𝑤) ∧ 𝑧 ∈ (1st𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥Q ∣ ∃𝑦Q𝑧Q (𝑦 ∈ (2nd𝑤) ∧ 𝑧 ∈ (2nd𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩)
genpelvl.2 ((𝑦Q𝑧Q) → (𝑦𝐺𝑧) ∈ Q)
genpcuu.2 ((((𝐴P𝑔 ∈ (2nd𝐴)) ∧ (𝐵P ∈ (2nd𝐵))) ∧ 𝑥Q) → ((𝑔𝐺) <Q 𝑥𝑥 ∈ (2nd ‘(𝐴𝐹𝐵))))
Assertion
Ref Expression
genpcuu ((𝐴P𝐵P) → (𝑓 ∈ (2nd ‘(𝐴𝐹𝐵)) → (𝑓 <Q 𝑥𝑥 ∈ (2nd ‘(𝐴𝐹𝐵)))))
Distinct variable groups:   𝑥,𝑦,𝑧,𝑓,𝑔,,𝑤,𝑣,𝐴   𝑥,𝐵,𝑦,𝑧,𝑓,𝑔,,𝑤,𝑣   𝑥,𝐺,𝑦,𝑧,𝑓,𝑔,,𝑤,𝑣   𝑓,𝐹,𝑔,
Allowed substitution hints:   𝐹(𝑥,𝑦,𝑧,𝑤,𝑣)

Proof of Theorem genpcuu
StepHypRef Expression
1 ltrelnq 6669 . . . . . . 7 <Q ⊆ (Q × Q)
21brel 4438 . . . . . 6 (𝑓 <Q 𝑥 → (𝑓Q𝑥Q))
32simprd 112 . . . . 5 (𝑓 <Q 𝑥𝑥Q)
4 genpelvl.1 . . . . . . . . 9 𝐹 = (𝑤P, 𝑣P ↦ ⟨{𝑥Q ∣ ∃𝑦Q𝑧Q (𝑦 ∈ (1st𝑤) ∧ 𝑧 ∈ (1st𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥Q ∣ ∃𝑦Q𝑧Q (𝑦 ∈ (2nd𝑤) ∧ 𝑧 ∈ (2nd𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩)
5 genpelvl.2 . . . . . . . . 9 ((𝑦Q𝑧Q) → (𝑦𝐺𝑧) ∈ Q)
64, 5genpelvu 6817 . . . . . . . 8 ((𝐴P𝐵P) → (𝑓 ∈ (2nd ‘(𝐴𝐹𝐵)) ↔ ∃𝑔 ∈ (2nd𝐴)∃ ∈ (2nd𝐵)𝑓 = (𝑔𝐺)))
76adantr 270 . . . . . . 7 (((𝐴P𝐵P) ∧ 𝑥Q) → (𝑓 ∈ (2nd ‘(𝐴𝐹𝐵)) ↔ ∃𝑔 ∈ (2nd𝐴)∃ ∈ (2nd𝐵)𝑓 = (𝑔𝐺)))
8 breq1 3808 . . . . . . . . . . . . 13 (𝑓 = (𝑔𝐺) → (𝑓 <Q 𝑥 ↔ (𝑔𝐺) <Q 𝑥))
98biimpd 142 . . . . . . . . . . . 12 (𝑓 = (𝑔𝐺) → (𝑓 <Q 𝑥 → (𝑔𝐺) <Q 𝑥))
10 genpcuu.2 . . . . . . . . . . . 12 ((((𝐴P𝑔 ∈ (2nd𝐴)) ∧ (𝐵P ∈ (2nd𝐵))) ∧ 𝑥Q) → ((𝑔𝐺) <Q 𝑥𝑥 ∈ (2nd ‘(𝐴𝐹𝐵))))
119, 10sylan9r 402 . . . . . . . . . . 11 (((((𝐴P𝑔 ∈ (2nd𝐴)) ∧ (𝐵P ∈ (2nd𝐵))) ∧ 𝑥Q) ∧ 𝑓 = (𝑔𝐺)) → (𝑓 <Q 𝑥𝑥 ∈ (2nd ‘(𝐴𝐹𝐵))))
1211exp31 356 . . . . . . . . . 10 (((𝐴P𝑔 ∈ (2nd𝐴)) ∧ (𝐵P ∈ (2nd𝐵))) → (𝑥Q → (𝑓 = (𝑔𝐺) → (𝑓 <Q 𝑥𝑥 ∈ (2nd ‘(𝐴𝐹𝐵))))))
1312an4s 553 . . . . . . . . 9 (((𝐴P𝐵P) ∧ (𝑔 ∈ (2nd𝐴) ∧ ∈ (2nd𝐵))) → (𝑥Q → (𝑓 = (𝑔𝐺) → (𝑓 <Q 𝑥𝑥 ∈ (2nd ‘(𝐴𝐹𝐵))))))
1413impancom 256 . . . . . . . 8 (((𝐴P𝐵P) ∧ 𝑥Q) → ((𝑔 ∈ (2nd𝐴) ∧ ∈ (2nd𝐵)) → (𝑓 = (𝑔𝐺) → (𝑓 <Q 𝑥𝑥 ∈ (2nd ‘(𝐴𝐹𝐵))))))
1514rexlimdvv 2488 . . . . . . 7 (((𝐴P𝐵P) ∧ 𝑥Q) → (∃𝑔 ∈ (2nd𝐴)∃ ∈ (2nd𝐵)𝑓 = (𝑔𝐺) → (𝑓 <Q 𝑥𝑥 ∈ (2nd ‘(𝐴𝐹𝐵)))))
167, 15sylbid 148 . . . . . 6 (((𝐴P𝐵P) ∧ 𝑥Q) → (𝑓 ∈ (2nd ‘(𝐴𝐹𝐵)) → (𝑓 <Q 𝑥𝑥 ∈ (2nd ‘(𝐴𝐹𝐵)))))
1716ex 113 . . . . 5 ((𝐴P𝐵P) → (𝑥Q → (𝑓 ∈ (2nd ‘(𝐴𝐹𝐵)) → (𝑓 <Q 𝑥𝑥 ∈ (2nd ‘(𝐴𝐹𝐵))))))
183, 17syl5 32 . . . 4 ((𝐴P𝐵P) → (𝑓 <Q 𝑥 → (𝑓 ∈ (2nd ‘(𝐴𝐹𝐵)) → (𝑓 <Q 𝑥𝑥 ∈ (2nd ‘(𝐴𝐹𝐵))))))
1918com34 82 . . 3 ((𝐴P𝐵P) → (𝑓 <Q 𝑥 → (𝑓 <Q 𝑥 → (𝑓 ∈ (2nd ‘(𝐴𝐹𝐵)) → 𝑥 ∈ (2nd ‘(𝐴𝐹𝐵))))))
2019pm2.43d 49 . 2 ((𝐴P𝐵P) → (𝑓 <Q 𝑥 → (𝑓 ∈ (2nd ‘(𝐴𝐹𝐵)) → 𝑥 ∈ (2nd ‘(𝐴𝐹𝐵)))))
2120com23 77 1 ((𝐴P𝐵P) → (𝑓 ∈ (2nd ‘(𝐴𝐹𝐵)) → (𝑓 <Q 𝑥𝑥 ∈ (2nd ‘(𝐴𝐹𝐵)))))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 102   ↔ wb 103   ∧ w3a 920   = wceq 1285   ∈ wcel 1434  ∃wrex 2354  {crab 2357  ⟨cop 3419   class class class wbr 3805  ‘cfv 4952  (class class class)co 5563   ↦ cmpt2 5565  1st c1st 5816  2nd c2nd 5817  Qcnq 6584
 Copyright terms: Public domain W3C validator