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

Theorem genpcdl 6495
 Description: Downward closure of an operation on positive reals. (Contributed by Jim Kingdon, 14-Oct-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)
genpcdl.2 ((((A P g (1stA)) (B P (1stB))) x Q) → (x <Q (g𝐺) → x (1st ‘(A𝐹B))))
Assertion
Ref Expression
genpcdl ((A P B P) → (f (1st ‘(A𝐹B)) → (x <Q fx (1st ‘(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 genpcdl
StepHypRef Expression
1 ltrelnq 6342 . . . . . . 7 <Q ⊆ (Q × Q)
21brel 4334 . . . . . 6 (x <Q f → (x Q f Q))
32simpld 105 . . . . 5 (x <Q fx 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, 5genpelvl 6487 . . . . . . . 8 ((A P B P) → (f (1st ‘(A𝐹B)) ↔ g (1stA) (1stB)f = (g𝐺)))
76adantr 261 . . . . . . 7 (((A P B P) x Q) → (f (1st ‘(A𝐹B)) ↔ g (1stA) (1stB)f = (g𝐺)))
8 breq2 3758 . . . . . . . . . . . . 13 (f = (g𝐺) → (x <Q fx <Q (g𝐺)))
98biimpd 132 . . . . . . . . . . . 12 (f = (g𝐺) → (x <Q fx <Q (g𝐺)))
10 genpcdl.2 . . . . . . . . . . . 12 ((((A P g (1stA)) (B P (1stB))) x Q) → (x <Q (g𝐺) → x (1st ‘(A𝐹B))))
119, 10sylan9r 390 . . . . . . . . . . 11 (((((A P g (1stA)) (B P (1stB))) x Q) f = (g𝐺)) → (x <Q fx (1st ‘(A𝐹B))))
1211exp31 346 . . . . . . . . . 10 (((A P g (1stA)) (B P (1stB))) → (x Q → (f = (g𝐺) → (x <Q fx (1st ‘(A𝐹B))))))
1312an4s 522 . . . . . . . . 9 (((A P B P) (g (1stA) (1stB))) → (x Q → (f = (g𝐺) → (x <Q fx (1st ‘(A𝐹B))))))
1413impancom 247 . . . . . . . 8 (((A P B P) x Q) → ((g (1stA) (1stB)) → (f = (g𝐺) → (x <Q fx (1st ‘(A𝐹B))))))
1514rexlimdvv 2433 . . . . . . 7 (((A P B P) x Q) → (g (1stA) (1stB)f = (g𝐺) → (x <Q fx (1st ‘(A𝐹B)))))
167, 15sylbid 139 . . . . . 6 (((A P B P) x Q) → (f (1st ‘(A𝐹B)) → (x <Q fx (1st ‘(A𝐹B)))))
1716ex 108 . . . . 5 ((A P B P) → (x Q → (f (1st ‘(A𝐹B)) → (x <Q fx (1st ‘(A𝐹B))))))
183, 17syl5 28 . . . 4 ((A P B P) → (x <Q f → (f (1st ‘(A𝐹B)) → (x <Q fx (1st ‘(A𝐹B))))))
1918com34 77 . . 3 ((A P B P) → (x <Q f → (x <Q f → (f (1st ‘(A𝐹B)) → x (1st ‘(A𝐹B))))))
2019pm2.43d 44 . 2 ((A P B P) → (x <Q f → (f (1st ‘(A𝐹B)) → x (1st ‘(A𝐹B)))))
2120com23 72 1 ((A P B P) → (f (1st ‘(A𝐹B)) → (x <Q fx (1st ‘(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 3369   class class class wbr 3754  ‘cfv 4844  (class class class)co 5452   ↦ cmpt2 5454  1st c1st 5704  2nd c2nd 5705  Qcnq 6257
 Copyright terms: Public domain W3C validator