addclpr - Intuitionistic Logic Explorer

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

Theorem addclpr 6513

Description: Closure of addition on positive reals. First statement of Proposition 9-3.5 of [Gleason] p. 123. Combination of Lemma 11.13 and Lemma 11.16 in [BauerTaylor], p. 53. (Contributed by NM, 13-Mar-1996.)

**Assertion**
Ref	Expression
addclpr	⊢ ((A ∈ P ∧ B ∈ P) → (A +_P B) ∈ P)

Proof of Theorem addclpr Dummy variables x y z w v g ℎ 𝑞 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-iplp 6443	. . . 4 ⊢ +_P = (w ∈ P, v ∈ P ↦ ⟨{x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (1^st ‘w) ∧ z ∈ (1^st ‘v) ∧ x = (y +_Q z))}, {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (2^nd ‘w) ∧ z ∈ (2^nd ‘v) ∧ x = (y +_Q z))}⟩)
2	1	genpelxp 6486	. . 3 ⊢ ((A ∈ P ∧ B ∈ P) → (A +_P B) ∈ (𝒫 Q × 𝒫 Q))
3		addclnq 6352	. . . 4 ⊢ ((y ∈ Q ∧ z ∈ Q) → (y +_Q z) ∈ Q)
4	1, 3	genpml 6493	. . 3 ⊢ ((A ∈ P ∧ B ∈ P) → ∃𝑞 ∈ Q 𝑞 ∈ (1^st ‘(A +_P B)))
5	1, 3	genpmu 6494	. . 3 ⊢ ((A ∈ P ∧ B ∈ P) → ∃𝑟 ∈ Q 𝑟 ∈ (2^nd ‘(A +_P B)))
6	2, 4, 5	jca32 293	. 2 ⊢ ((A ∈ P ∧ B ∈ P) → ((A +_P B) ∈ (𝒫 Q × 𝒫 Q) ∧ (∃𝑞 ∈ Q 𝑞 ∈ (1^st ‘(A +_P B)) ∧ ∃𝑟 ∈ Q 𝑟 ∈ (2^nd ‘(A +_P B)))))
7		ltanqg 6377	. . . . 5 ⊢ ((x ∈ Q ∧ y ∈ Q ∧ z ∈ Q) → (x <_Q y ↔ (z +_Q x) <_Q (z +_Q y)))
8		addcomnqg 6358	. . . . 5 ⊢ ((x ∈ Q ∧ y ∈ Q) → (x +_Q y) = (y +_Q x))
9		addnqprl 6505	. . . . 5 ⊢ ((((A ∈ P ∧ g ∈ (1^st ‘A)) ∧ (B ∈ P ∧ ℎ ∈ (1^st ‘B))) ∧ x ∈ Q) → (x <_Q (g +_Q ℎ) → x ∈ (1^st ‘(A +_P B))))
10	1, 3, 7, 8, 9	genprndl 6497	. . . 4 ⊢ ((A ∈ P ∧ B ∈ P) → ∀𝑞 ∈ Q (𝑞 ∈ (1^st ‘(A +_P B)) ↔ ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘(A +_P B)))))
11		addnqpru 6506	. . . . 5 ⊢ ((((A ∈ P ∧ g ∈ (2^nd ‘A)) ∧ (B ∈ P ∧ ℎ ∈ (2^nd ‘B))) ∧ x ∈ Q) → ((g +_Q ℎ) <_Q x → x ∈ (2^nd ‘(A +_P B))))
12	1, 3, 7, 8, 11	genprndu 6498	. . . 4 ⊢ ((A ∈ P ∧ B ∈ P) → ∀𝑟 ∈ Q (𝑟 ∈ (2^nd ‘(A +_P B)) ↔ ∃𝑞 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑞 ∈ (2^nd ‘(A +_P B)))))
13	10, 12	jca 290	. . 3 ⊢ ((A ∈ P ∧ B ∈ P) → (∀𝑞 ∈ Q (𝑞 ∈ (1^st ‘(A +_P B)) ↔ ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘(A +_P B)))) ∧ ∀𝑟 ∈ Q (𝑟 ∈ (2^nd ‘(A +_P B)) ↔ ∃𝑞 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑞 ∈ (2^nd ‘(A +_P B))))))
14	1, 3, 7, 8	genpdisj 6499	. . 3 ⊢ ((A ∈ P ∧ B ∈ P) → ∀𝑞 ∈ Q ¬ (𝑞 ∈ (1^st ‘(A +_P B)) ∧ 𝑞 ∈ (2^nd ‘(A +_P B))))
15		addlocpr 6512	. . 3 ⊢ ((A ∈ P ∧ B ∈ P) → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <_Q 𝑟 → (𝑞 ∈ (1^st ‘(A +_P B)) ∨ 𝑟 ∈ (2^nd ‘(A +_P B)))))
16	13, 14, 15	3jca 1083	. 2 ⊢ ((A ∈ P ∧ B ∈ P) → ((∀𝑞 ∈ Q (𝑞 ∈ (1^st ‘(A +_P B)) ↔ ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘(A +_P B)))) ∧ ∀𝑟 ∈ Q (𝑟 ∈ (2^nd ‘(A +_P B)) ↔ ∃𝑞 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑞 ∈ (2^nd ‘(A +_P B))))) ∧ ∀𝑞 ∈ Q ¬ (𝑞 ∈ (1^st ‘(A +_P B)) ∧ 𝑞 ∈ (2^nd ‘(A +_P B))) ∧ ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <_Q 𝑟 → (𝑞 ∈ (1^st ‘(A +_P B)) ∨ 𝑟 ∈ (2^nd ‘(A +_P B))))))
17		elnp1st2nd 6451	. 2 ⊢ ((A +_P B) ∈ P ↔ (((A +_P B) ∈ (𝒫 Q × 𝒫 Q) ∧ (∃𝑞 ∈ Q 𝑞 ∈ (1^st ‘(A +_P B)) ∧ ∃𝑟 ∈ Q 𝑟 ∈ (2^nd ‘(A +_P B)))) ∧ ((∀𝑞 ∈ Q (𝑞 ∈ (1^st ‘(A +_P B)) ↔ ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘(A +_P B)))) ∧ ∀𝑟 ∈ Q (𝑟 ∈ (2^nd ‘(A +_P B)) ↔ ∃𝑞 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑞 ∈ (2^nd ‘(A +_P B))))) ∧ ∀𝑞 ∈ Q ¬ (𝑞 ∈ (1^st ‘(A +_P B)) ∧ 𝑞 ∈ (2^nd ‘(A +_P B))) ∧ ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <_Q 𝑟 → (𝑞 ∈ (1^st ‘(A +_P B)) ∨ 𝑟 ∈ (2^nd ‘(A +_P B)))))))
18	6, 16, 17	sylanbrc 394	1 ⊢ ((A ∈ P ∧ B ∈ P) → (A +_P B) ∈ P)

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 97 ↔ wb 98 ∨ wo 628 ∧ w3a 884 ∈ wcel 1390 ∀wral 2300 ∃wrex 2301 𝒫 cpw 3350 class class class wbr 3754 × cxp 4285 ‘cfv 4844 (class class class)co 5452 1^st c1st 5704 2^nd c2nd 5705 Qcnq 6257 +_Q cplq 6259 <_Q cltq 6262 Pcnp 6268 +_P cpp 6270

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-in1 544 ax-in2 545 ax-io 629 ax-5 1333 ax-7 1334 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-8 1392 ax-10 1393 ax-11 1394 ax-i12 1395 ax-bnd 1396 ax-4 1397 ax-13 1401 ax-14 1402 ax-17 1416 ax-i9 1420 ax-ial 1424 ax-i5r 1425 ax-ext 2019 ax-coll 3862 ax-sep 3865 ax-nul 3873 ax-pow 3917 ax-pr 3934 ax-un 4135 ax-setind 4219 ax-iinf 4253

This theorem depends on definitions: df-bi 110 df-dc 742 df-3or 885 df-3an 886 df-tru 1245 df-fal 1248 df-nf 1347 df-sb 1643 df-eu 1900 df-mo 1901 df-clab 2024 df-cleq 2030 df-clel 2033 df-nfc 2164 df-ne 2203 df-ral 2305 df-rex 2306 df-reu 2307 df-rab 2309 df-v 2553 df-sbc 2759 df-csb 2847 df-dif 2914 df-un 2916 df-in 2918 df-ss 2925 df-nul 3219 df-pw 3352 df-sn 3372 df-pr 3373 df-op 3375 df-uni 3571 df-int 3606 df-iun 3649 df-br 3755 df-opab 3809 df-mpt 3810 df-tr 3845 df-eprel 4016 df-id 4020 df-po 4023 df-iso 4024 df-iord 4068 df-on 4070 df-suc 4073 df-iom 4256 df-xp 4293 df-rel 4294 df-cnv 4295 df-co 4296 df-dm 4297 df-rn 4298 df-res 4299 df-ima 4300 df-iota 4809 df-fun 4846 df-fn 4847 df-f 4848 df-f1 4849 df-fo 4850 df-f1o 4851 df-fv 4852 df-ov 5455 df-oprab 5456 df-mpt2 5457 df-1st 5706 df-2nd 5707 df-recs 5858 df-irdg 5894 df-1o 5933 df-2o 5934 df-oadd 5937 df-omul 5938 df-er 6035 df-ec 6037 df-qs 6041 df-ni 6281 df-pli 6282 df-mi 6283 df-lti 6284 df-plpq 6321 df-mpq 6322 df-enq 6324 df-nqqs 6325 df-plqqs 6326 df-mqqs 6327 df-1nqqs 6328 df-rq 6329 df-ltnqqs 6330 df-enq0 6399 df-nq0 6400 df-0nq0 6401 df-plq0 6402 df-mq0 6403 df-inp 6441 df-iplp 6443

This theorem is referenced by: addnqpr1lemil 6531 addnqpr1lemiu 6532 addnqpr1 6533 addassprg 6545 distrlem1prl 6548 distrlem1pru 6549 distrlem4prl 6550 distrlem4pru 6551 distrprg 6554 ltaddpr 6561 ltexpri 6577 addcanprleml 6578 addcanprlemu 6579 ltaprlem 6581 ltaprg 6582 addextpr 6583 enrer 6615 addcmpblnr 6619 mulcmpblnrlemg 6620 mulcmpblnr 6621 ltsrprg 6627 1sr 6631 m1r 6632 addclsr 6633 mulclsr 6634 addasssrg 6636 mulasssrg 6638 distrsrg 6639 m1p1sr 6640 m1m1sr 6641 lttrsr 6642 ltsosr 6644 0lt1sr 6645 0idsr 6647 1idsr 6648 00sr 6649 ltasrg 6650 recexgt0sr 6653 mulgt0sr 6656 aptisr 6657 mulextsr1lem 6658 mulextsr1 6659 archsr 6660 pitonnlem1p1 6694 pitonnlem2 6695 pitonn 6696

W3C validator