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

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

Proof of Theorem genpcdl
StepHypRef Expression
1 ltrelnq 6463 . . . . . . 7 <Q ⊆ (Q × Q)
21brel 4392 . . . . . 6 (𝑥 <Q 𝑓 → (𝑥Q𝑓Q))
32simpld 105 . . . . 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, 5genpelvl 6610 . . . . . . . 8 ((𝐴P𝐵P) → (𝑓 ∈ (1st ‘(𝐴𝐹𝐵)) ↔ ∃𝑔 ∈ (1st𝐴)∃ ∈ (1st𝐵)𝑓 = (𝑔𝐺)))
76adantr 261 . . . . . . 7 (((𝐴P𝐵P) ∧ 𝑥Q) → (𝑓 ∈ (1st ‘(𝐴𝐹𝐵)) ↔ ∃𝑔 ∈ (1st𝐴)∃ ∈ (1st𝐵)𝑓 = (𝑔𝐺)))
8 breq2 3768 . . . . . . . . . . . . 13 (𝑓 = (𝑔𝐺) → (𝑥 <Q 𝑓𝑥 <Q (𝑔𝐺)))
98biimpd 132 . . . . . . . . . . . 12 (𝑓 = (𝑔𝐺) → (𝑥 <Q 𝑓𝑥 <Q (𝑔𝐺)))
10 genpcdl.2 . . . . . . . . . . . 12 ((((𝐴P𝑔 ∈ (1st𝐴)) ∧ (𝐵P ∈ (1st𝐵))) ∧ 𝑥Q) → (𝑥 <Q (𝑔𝐺) → 𝑥 ∈ (1st ‘(𝐴𝐹𝐵))))
119, 10sylan9r 390 . . . . . . . . . . 11 (((((𝐴P𝑔 ∈ (1st𝐴)) ∧ (𝐵P ∈ (1st𝐵))) ∧ 𝑥Q) ∧ 𝑓 = (𝑔𝐺)) → (𝑥 <Q 𝑓𝑥 ∈ (1st ‘(𝐴𝐹𝐵))))
1211exp31 346 . . . . . . . . . 10 (((𝐴P𝑔 ∈ (1st𝐴)) ∧ (𝐵P ∈ (1st𝐵))) → (𝑥Q → (𝑓 = (𝑔𝐺) → (𝑥 <Q 𝑓𝑥 ∈ (1st ‘(𝐴𝐹𝐵))))))
1312an4s 522 . . . . . . . . 9 (((𝐴P𝐵P) ∧ (𝑔 ∈ (1st𝐴) ∧ ∈ (1st𝐵))) → (𝑥Q → (𝑓 = (𝑔𝐺) → (𝑥 <Q 𝑓𝑥 ∈ (1st ‘(𝐴𝐹𝐵))))))
1413impancom 247 . . . . . . . 8 (((𝐴P𝐵P) ∧ 𝑥Q) → ((𝑔 ∈ (1st𝐴) ∧ ∈ (1st𝐵)) → (𝑓 = (𝑔𝐺) → (𝑥 <Q 𝑓𝑥 ∈ (1st ‘(𝐴𝐹𝐵))))))
1514rexlimdvv 2439 . . . . . . 7 (((𝐴P𝐵P) ∧ 𝑥Q) → (∃𝑔 ∈ (1st𝐴)∃ ∈ (1st𝐵)𝑓 = (𝑔𝐺) → (𝑥 <Q 𝑓𝑥 ∈ (1st ‘(𝐴𝐹𝐵)))))
167, 15sylbid 139 . . . . . 6 (((𝐴P𝐵P) ∧ 𝑥Q) → (𝑓 ∈ (1st ‘(𝐴𝐹𝐵)) → (𝑥 <Q 𝑓𝑥 ∈ (1st ‘(𝐴𝐹𝐵)))))
1716ex 108 . . . . 5 ((𝐴P𝐵P) → (𝑥Q → (𝑓 ∈ (1st ‘(𝐴𝐹𝐵)) → (𝑥 <Q 𝑓𝑥 ∈ (1st ‘(𝐴𝐹𝐵))))))
183, 17syl5 28 . . . 4 ((𝐴P𝐵P) → (𝑥 <Q 𝑓 → (𝑓 ∈ (1st ‘(𝐴𝐹𝐵)) → (𝑥 <Q 𝑓𝑥 ∈ (1st ‘(𝐴𝐹𝐵))))))
1918com34 77 . . 3 ((𝐴P𝐵P) → (𝑥 <Q 𝑓 → (𝑥 <Q 𝑓 → (𝑓 ∈ (1st ‘(𝐴𝐹𝐵)) → 𝑥 ∈ (1st ‘(𝐴𝐹𝐵))))))
2019pm2.43d 44 . 2 ((𝐴P𝐵P) → (𝑥 <Q 𝑓 → (𝑓 ∈ (1st ‘(𝐴𝐹𝐵)) → 𝑥 ∈ (1st ‘(𝐴𝐹𝐵)))))
2120com23 72 1 ((𝐴P𝐵P) → (𝑓 ∈ (1st ‘(𝐴𝐹𝐵)) → (𝑥 <Q 𝑓𝑥 ∈ (1st ‘(𝐴𝐹𝐵)))))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∧ w3a 885   = wceq 1243   ∈ wcel 1393  ∃wrex 2307  {crab 2310  ⟨cop 3378   class class class wbr 3764  ‘cfv 4902  (class class class)co 5512   ↦ cmpt2 5514  1st c1st 5765  2nd c2nd 5766  Qcnq 6378
 Copyright terms: Public domain W3C validator