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

Theorem recexprlempr 6604
 Description: B is a positive real. Lemma for recexpr 6610. (Contributed by Jim Kingdon, 27-Dec-2019.)
Hypothesis
Ref Expression
recexpr.1 B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩
Assertion
Ref Expression
recexprlempr (A PB P)
Distinct variable groups:   x,y,A   x,B,y

Proof of Theorem recexprlempr
Dummy variables 𝑟 𝑞 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 recexpr.1 . . . 4 B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩
21recexprlemm 6596 . . 3 (A P → (𝑞 Q 𝑞 (1stB) 𝑟 Q 𝑟 (2ndB)))
3 ltrelnq 6349 . . . . . . . . . . 11 <Q ⊆ (Q × Q)
43brel 4335 . . . . . . . . . 10 (x <Q y → (x Q y Q))
54simpld 105 . . . . . . . . 9 (x <Q yx Q)
65adantr 261 . . . . . . . 8 ((x <Q y (*Qy) (2ndA)) → x Q)
76exlimiv 1486 . . . . . . 7 (y(x <Q y (*Qy) (2ndA)) → x Q)
87abssi 3009 . . . . . 6 {xy(x <Q y (*Qy) (2ndA))} ⊆ Q
9 nqex 6347 . . . . . . 7 Q V
109elpw2 3902 . . . . . 6 ({xy(x <Q y (*Qy) (2ndA))} 𝒫 Q ↔ {xy(x <Q y (*Qy) (2ndA))} ⊆ Q)
118, 10mpbir 134 . . . . 5 {xy(x <Q y (*Qy) (2ndA))} 𝒫 Q
123brel 4335 . . . . . . . . . 10 (y <Q x → (y Q x Q))
1312simprd 107 . . . . . . . . 9 (y <Q xx Q)
1413adantr 261 . . . . . . . 8 ((y <Q x (*Qy) (1stA)) → x Q)
1514exlimiv 1486 . . . . . . 7 (y(y <Q x (*Qy) (1stA)) → x Q)
1615abssi 3009 . . . . . 6 {xy(y <Q x (*Qy) (1stA))} ⊆ Q
179elpw2 3902 . . . . . 6 ({xy(y <Q x (*Qy) (1stA))} 𝒫 Q ↔ {xy(y <Q x (*Qy) (1stA))} ⊆ Q)
1816, 17mpbir 134 . . . . 5 {xy(y <Q x (*Qy) (1stA))} 𝒫 Q
19 opelxpi 4319 . . . . 5 (({xy(x <Q y (*Qy) (2ndA))} 𝒫 Q {xy(y <Q x (*Qy) (1stA))} 𝒫 Q) → ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩ (𝒫 Q × 𝒫 Q))
2011, 18, 19mp2an 402 . . . 4 ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩ (𝒫 Q × 𝒫 Q)
211, 20eqeltri 2107 . . 3 B (𝒫 Q × 𝒫 Q)
222, 21jctil 295 . 2 (A P → (B (𝒫 Q × 𝒫 Q) (𝑞 Q 𝑞 (1stB) 𝑟 Q 𝑟 (2ndB))))
231recexprlemrnd 6601 . . 3 (A P → (𝑞 Q (𝑞 (1stB) ↔ 𝑟 Q (𝑞 <Q 𝑟 𝑟 (1stB))) 𝑟 Q (𝑟 (2ndB) ↔ 𝑞 Q (𝑞 <Q 𝑟 𝑞 (2ndB)))))
241recexprlemdisj 6602 . . 3 (A P𝑞 Q ¬ (𝑞 (1stB) 𝑞 (2ndB)))
251recexprlemloc 6603 . . 3 (A P𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 (1stB) 𝑟 (2ndB))))
2623, 24, 253jca 1083 . 2 (A P → ((𝑞 Q (𝑞 (1stB) ↔ 𝑟 Q (𝑞 <Q 𝑟 𝑟 (1stB))) 𝑟 Q (𝑟 (2ndB) ↔ 𝑞 Q (𝑞 <Q 𝑟 𝑞 (2ndB)))) 𝑞 Q ¬ (𝑞 (1stB) 𝑞 (2ndB)) 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 (1stB) 𝑟 (2ndB)))))
27 elnp1st2nd 6459 . 2 (B P ↔ ((B (𝒫 Q × 𝒫 Q) (𝑞 Q 𝑞 (1stB) 𝑟 Q 𝑟 (2ndB))) ((𝑞 Q (𝑞 (1stB) ↔ 𝑟 Q (𝑞 <Q 𝑟 𝑟 (1stB))) 𝑟 Q (𝑟 (2ndB) ↔ 𝑞 Q (𝑞 <Q 𝑟 𝑞 (2ndB)))) 𝑞 Q ¬ (𝑞 (1stB) 𝑞 (2ndB)) 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 (1stB) 𝑟 (2ndB))))))
2822, 26, 27sylanbrc 394 1 (A PB P)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 628   ∧ w3a 884   = wceq 1242  ∃wex 1378   ∈ wcel 1390  {cab 2023  ∀wral 2300  ∃wrex 2301   ⊆ wss 2911  𝒫 cpw 3351  ⟨cop 3370   class class class wbr 3755   × cxp 4286  ‘cfv 4845  1st c1st 5707  2nd c2nd 5708  Qcnq 6264  *Qcrq 6268
 Copyright terms: Public domain W3C validator