ixxss1 - Intuitionistic Logic Explorer

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

Theorem ixxss1 9717

Description: Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 28-Apr-2015.)

**Hypotheses**
Ref	Expression
ixxssixx.1	⊢ 𝑂 = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)})
ixxss1.2	⊢ 𝑃 = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑆𝑦)})
ixxss1.3	⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) → ((𝐴𝑊𝐵 ∧ 𝐵𝑇𝑤) → 𝐴𝑅𝑤))

**Assertion**
Ref	Expression
ixxss1	⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴𝑊𝐵) → (𝐵𝑃𝐶) ⊆ (𝐴𝑂𝐶))

Distinct variable groups: 𝑥,𝑤,𝑦,𝑧,𝐴 𝑤,𝐶,𝑥,𝑦,𝑧 𝑤,𝑂,𝑥 𝑤,𝐵,𝑥,𝑦,𝑧 𝑤,𝑃 𝑥,𝑅,𝑦,𝑧 𝑥,𝑆,𝑦,𝑧 𝑥,𝑇,𝑦,𝑧 𝑤,𝑊 Allowed substitution hints: 𝑃(𝑥,𝑦,𝑧) 𝑅(𝑤) 𝑆(𝑤) 𝑇(𝑤) 𝑂(𝑦,𝑧) 𝑊(𝑥,𝑦,𝑧)

**Proof of Theorem ixxss1**
Step	Hyp	Ref	Expression
1		ixxss1.2	. . . . . . . 8 ⊢ 𝑃 = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑆𝑦)})
2	1	elixx3g 9714	. . . . . . 7 ⊢ (𝑤 ∈ (𝐵𝑃𝐶) ↔ ((𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝐵𝑇𝑤 ∧ 𝑤𝑆𝐶)))
3	2	simplbi 272	. . . . . 6 ⊢ (𝑤 ∈ (𝐵𝑃𝐶) → (𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*))
4	3	adantl 275	. . . . 5 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐴𝑊𝐵) ∧ 𝑤 ∈ (𝐵𝑃𝐶)) → (𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*))
5	4	simp3d 996	. . . 4 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐴𝑊𝐵) ∧ 𝑤 ∈ (𝐵𝑃𝐶)) → 𝑤 ∈ ℝ^*)
6		simplr 520	. . . . 5 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐴𝑊𝐵) ∧ 𝑤 ∈ (𝐵𝑃𝐶)) → 𝐴𝑊𝐵)
7	2	simprbi 273	. . . . . . 7 ⊢ (𝑤 ∈ (𝐵𝑃𝐶) → (𝐵𝑇𝑤 ∧ 𝑤𝑆𝐶))
8	7	adantl 275	. . . . . 6 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐴𝑊𝐵) ∧ 𝑤 ∈ (𝐵𝑃𝐶)) → (𝐵𝑇𝑤 ∧ 𝑤𝑆𝐶))
9	8	simpld 111	. . . . 5 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐴𝑊𝐵) ∧ 𝑤 ∈ (𝐵𝑃𝐶)) → 𝐵𝑇𝑤)
10		simpll 519	. . . . . 6 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐴𝑊𝐵) ∧ 𝑤 ∈ (𝐵𝑃𝐶)) → 𝐴 ∈ ℝ^*)
11	4	simp1d 994	. . . . . 6 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐴𝑊𝐵) ∧ 𝑤 ∈ (𝐵𝑃𝐶)) → 𝐵 ∈ ℝ^*)
12		ixxss1.3	. . . . . 6 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) → ((𝐴𝑊𝐵 ∧ 𝐵𝑇𝑤) → 𝐴𝑅𝑤))
13	10, 11, 5, 12	syl3anc 1217	. . . . 5 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐴𝑊𝐵) ∧ 𝑤 ∈ (𝐵𝑃𝐶)) → ((𝐴𝑊𝐵 ∧ 𝐵𝑇𝑤) → 𝐴𝑅𝑤))
14	6, 9, 13	mp2and 430	. . . 4 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐴𝑊𝐵) ∧ 𝑤 ∈ (𝐵𝑃𝐶)) → 𝐴𝑅𝑤)
15	8	simprd 113	. . . 4 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐴𝑊𝐵) ∧ 𝑤 ∈ (𝐵𝑃𝐶)) → 𝑤𝑆𝐶)
16	4	simp2d 995	. . . . 5 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐴𝑊𝐵) ∧ 𝑤 ∈ (𝐵𝑃𝐶)) → 𝐶 ∈ ℝ^*)
17		ixxssixx.1	. . . . . 6 ⊢ 𝑂 = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)})
18	17	elixx1 9710	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^) → (𝑤 ∈ (𝐴𝑂𝐶) ↔ (𝑤 ∈ ℝ^ ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐶)))
19	10, 16, 18	syl2anc 409	. . . 4 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐴𝑊𝐵) ∧ 𝑤 ∈ (𝐵𝑃𝐶)) → (𝑤 ∈ (𝐴𝑂𝐶) ↔ (𝑤 ∈ ℝ^* ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐶)))
20	5, 14, 15, 19	mpbir3and 1165	. . 3 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐴𝑊𝐵) ∧ 𝑤 ∈ (𝐵𝑃𝐶)) → 𝑤 ∈ (𝐴𝑂𝐶))
21	20	ex 114	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴𝑊𝐵) → (𝑤 ∈ (𝐵𝑃𝐶) → 𝑤 ∈ (𝐴𝑂𝐶)))
22	21	ssrdv 3108	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴𝑊𝐵) → (𝐵𝑃𝐶) ⊆ (𝐴𝑂𝐶))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 ∧ w3a 963 = wceq 1332 ∈ wcel 1481 {crab 2421 ⊆ wss 3076 class class class wbr 3937 (class class class)co 5782 ∈ cmpo 5784 ℝ^*cxr 7823

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-13 1492 ax-14 1493 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 ax-sep 4054 ax-pow 4106 ax-pr 4139 ax-un 4363 ax-setind 4460 ax-cnex 7735 ax-resscn 7736

This theorem depends on definitions: df-bi 116 df-3an 965 df-tru 1335 df-fal 1338 df-nf 1438 df-sb 1737 df-eu 2003 df-mo 2004 df-clab 2127 df-cleq 2133 df-clel 2136 df-nfc 2271 df-ne 2310 df-ral 2422 df-rex 2423 df-rab 2426 df-v 2691 df-sbc 2914 df-dif 3078 df-un 3080 df-in 3082 df-ss 3089 df-pw 3517 df-sn 3538 df-pr 3539 df-op 3541 df-uni 3745 df-br 3938 df-opab 3998 df-id 4223 df-xp 4553 df-rel 4554 df-cnv 4555 df-co 4556 df-dm 4557 df-iota 5096 df-fun 5133 df-fv 5139 df-ov 5785 df-oprab 5786 df-mpo 5787 df-pnf 7826 df-mnf 7827 df-xr 7828

This theorem is referenced by: iooss1 9729

W3C validator