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

Theorem npsspw 6319
 Description: Lemma for proving existence of reals. (Contributed by Jim Kingdon, 27-Sep-2019.)
Assertion
Ref Expression
npsspw P ⊆ (𝒫 Q × 𝒫 Q)

Proof of Theorem npsspw
Dummy variables u 𝑙 𝑞 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpll 469 . . . 4 ((((𝑙Q uQ) (𝑞 Q 𝑞 𝑙 𝑟 Q 𝑟 u)) ((𝑞 Q (𝑞 𝑙𝑟 Q (𝑞 <Q 𝑟 𝑟 𝑙)) 𝑟 Q (𝑟 u𝑞 Q (𝑞 <Q 𝑟 𝑞 u))) 𝑞 Q ¬ (𝑞 𝑙 𝑞 u) 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 𝑙 𝑟 u)))) → (𝑙Q uQ))
2 selpw 3337 . . . . 5 (𝑙 𝒫 Q𝑙Q)
3 selpw 3337 . . . . 5 (u 𝒫 QuQ)
42, 3anbi12i 436 . . . 4 ((𝑙 𝒫 Q u 𝒫 Q) ↔ (𝑙Q uQ))
51, 4sylibr 137 . . 3 ((((𝑙Q uQ) (𝑞 Q 𝑞 𝑙 𝑟 Q 𝑟 u)) ((𝑞 Q (𝑞 𝑙𝑟 Q (𝑞 <Q 𝑟 𝑟 𝑙)) 𝑟 Q (𝑟 u𝑞 Q (𝑞 <Q 𝑟 𝑞 u))) 𝑞 Q ¬ (𝑞 𝑙 𝑞 u) 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 𝑙 𝑟 u)))) → (𝑙 𝒫 Q u 𝒫 Q))
65ssopab2i 3984 . 2 {⟨𝑙, u⟩ ∣ (((𝑙Q uQ) (𝑞 Q 𝑞 𝑙 𝑟 Q 𝑟 u)) ((𝑞 Q (𝑞 𝑙𝑟 Q (𝑞 <Q 𝑟 𝑟 𝑙)) 𝑟 Q (𝑟 u𝑞 Q (𝑞 <Q 𝑟 𝑞 u))) 𝑞 Q ¬ (𝑞 𝑙 𝑞 u) 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 𝑙 𝑟 u))))} ⊆ {⟨𝑙, u⟩ ∣ (𝑙 𝒫 Q u 𝒫 Q)}
7 df-inp 6314 . 2 P = {⟨𝑙, u⟩ ∣ (((𝑙Q uQ) (𝑞 Q 𝑞 𝑙 𝑟 Q 𝑟 u)) ((𝑞 Q (𝑞 𝑙𝑟 Q (𝑞 <Q 𝑟 𝑟 𝑙)) 𝑟 Q (𝑟 u𝑞 Q (𝑞 <Q 𝑟 𝑞 u))) 𝑞 Q ¬ (𝑞 𝑙 𝑞 u) 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 𝑙 𝑟 u))))}
8 df-xp 4274 . 2 (𝒫 Q × 𝒫 Q) = {⟨𝑙, u⟩ ∣ (𝑙 𝒫 Q u 𝒫 Q)}
96, 7, 83sstr4i 2957 1 P ⊆ (𝒫 Q × 𝒫 Q)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 616   ∧ w3a 871   ∈ wcel 1370  ∀wral 2280  ∃wrex 2281   ⊆ wss 2890  𝒫 cpw 3330   class class class wbr 3734  {copab 3787   × cxp 4266  Qcnq 6134
 Copyright terms: Public domain W3C validator