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

Theorem genpcuu 6503
 Description: Upward closure of an operation on positive reals. (Contributed by Jim Kingdon, 8-Nov-2019.)
Hypotheses
Ref Expression
genpelvl.1 𝐹 = (w P, v P ↦ ⟨{x Qy Q z Q (y (1stw) z (1stv) x = (y𝐺z))}, {x Qy Q z Q (y (2ndw) z (2ndv) x = (y𝐺z))}⟩)
genpelvl.2 ((y Q z Q) → (y𝐺z) Q)
genpcuu.2 ((((A P g (2ndA)) (B P (2ndB))) x Q) → ((g𝐺) <Q xx (2nd ‘(A𝐹B))))
Assertion
Ref Expression
genpcuu ((A P B P) → (f (2nd ‘(A𝐹B)) → (f <Q xx (2nd ‘(A𝐹B)))))
Distinct variable groups:   x,y,z,f,g,,w,v,A   x,B,y,z,f,g,,w,v   x,𝐺,y,z,f,g,,w,v   f,𝐹,g,
Allowed substitution hints:   𝐹(x,y,z,w,v)

Proof of Theorem genpcuu
StepHypRef Expression
1 ltrelnq 6349 . . . . . . 7 <Q ⊆ (Q × Q)
21brel 4335 . . . . . 6 (f <Q x → (f Q x Q))
32simprd 107 . . . . 5 (f <Q xx Q)
4 genpelvl.1 . . . . . . . . 9 𝐹 = (w P, v P ↦ ⟨{x Qy Q z Q (y (1stw) z (1stv) x = (y𝐺z))}, {x Qy Q z Q (y (2ndw) z (2ndv) x = (y𝐺z))}⟩)
5 genpelvl.2 . . . . . . . . 9 ((y Q z Q) → (y𝐺z) Q)
64, 5genpelvu 6496 . . . . . . . 8 ((A P B P) → (f (2nd ‘(A𝐹B)) ↔ g (2ndA) (2ndB)f = (g𝐺)))
76adantr 261 . . . . . . 7 (((A P B P) x Q) → (f (2nd ‘(A𝐹B)) ↔ g (2ndA) (2ndB)f = (g𝐺)))
8 breq1 3758 . . . . . . . . . . . . 13 (f = (g𝐺) → (f <Q x ↔ (g𝐺) <Q x))
98biimpd 132 . . . . . . . . . . . 12 (f = (g𝐺) → (f <Q x → (g𝐺) <Q x))
10 genpcuu.2 . . . . . . . . . . . 12 ((((A P g (2ndA)) (B P (2ndB))) x Q) → ((g𝐺) <Q xx (2nd ‘(A𝐹B))))
119, 10sylan9r 390 . . . . . . . . . . 11 (((((A P g (2ndA)) (B P (2ndB))) x Q) f = (g𝐺)) → (f <Q xx (2nd ‘(A𝐹B))))
1211exp31 346 . . . . . . . . . 10 (((A P g (2ndA)) (B P (2ndB))) → (x Q → (f = (g𝐺) → (f <Q xx (2nd ‘(A𝐹B))))))
1312an4s 522 . . . . . . . . 9 (((A P B P) (g (2ndA) (2ndB))) → (x Q → (f = (g𝐺) → (f <Q xx (2nd ‘(A𝐹B))))))
1413impancom 247 . . . . . . . 8 (((A P B P) x Q) → ((g (2ndA) (2ndB)) → (f = (g𝐺) → (f <Q xx (2nd ‘(A𝐹B))))))
1514rexlimdvv 2433 . . . . . . 7 (((A P B P) x Q) → (g (2ndA) (2ndB)f = (g𝐺) → (f <Q xx (2nd ‘(A𝐹B)))))
167, 15sylbid 139 . . . . . 6 (((A P B P) x Q) → (f (2nd ‘(A𝐹B)) → (f <Q xx (2nd ‘(A𝐹B)))))
1716ex 108 . . . . 5 ((A P B P) → (x Q → (f (2nd ‘(A𝐹B)) → (f <Q xx (2nd ‘(A𝐹B))))))
183, 17syl5 28 . . . 4 ((A P B P) → (f <Q x → (f (2nd ‘(A𝐹B)) → (f <Q xx (2nd ‘(A𝐹B))))))
1918com34 77 . . 3 ((A P B P) → (f <Q x → (f <Q x → (f (2nd ‘(A𝐹B)) → x (2nd ‘(A𝐹B))))))
2019pm2.43d 44 . 2 ((A P B P) → (f <Q x → (f (2nd ‘(A𝐹B)) → x (2nd ‘(A𝐹B)))))
2120com23 72 1 ((A P B P) → (f (2nd ‘(A𝐹B)) → (f <Q xx (2nd ‘(A𝐹B)))))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∧ w3a 884   = wceq 1242   ∈ wcel 1390  ∃wrex 2301  {crab 2304  ⟨cop 3370   class class class wbr 3755  ‘cfv 4845  (class class class)co 5455   ↦ cmpt2 5457  1st c1st 5707  2nd c2nd 5708  Qcnq 6264
 Copyright terms: Public domain W3C validator