ixxssixx - Intuitionistic Logic Explorer

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

Theorem ixxssixx 9904

Description: An interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)

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

**Assertion**
Ref	Expression
ixxssixx	⊢ (𝐴𝑂𝐵) ⊆ (𝐴𝑃𝐵)

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

**Proof of Theorem ixxssixx**
Step	Hyp	Ref	Expression
1		ixxssixx.1	. . . 4 ⊢ 𝑂 = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)})
2	1	elmpocl 6071	. . 3 ⊢ (𝑤 ∈ (𝐴𝑂𝐵) → (𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*))
3		simp1 997	. . . . . 6 ⊢ ((𝑤 ∈ ℝ^* ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵) → 𝑤 ∈ ℝ^*)
4	3	a1i 9	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → ((𝑤 ∈ ℝ^ ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵) → 𝑤 ∈ ℝ^*))
5		simpl 109	. . . . . 6 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → 𝐴 ∈ ℝ^)
6		3simpa 994	. . . . . 6 ⊢ ((𝑤 ∈ ℝ^* ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵) → (𝑤 ∈ ℝ^* ∧ 𝐴𝑅𝑤))
7		ixx.3	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) → (𝐴𝑅𝑤 → 𝐴𝑇𝑤))
8	7	expimpd 363	. . . . . 6 ⊢ (𝐴 ∈ ℝ^* → ((𝑤 ∈ ℝ^* ∧ 𝐴𝑅𝑤) → 𝐴𝑇𝑤))
9	5, 6, 8	syl2im 38	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → ((𝑤 ∈ ℝ^ ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵) → 𝐴𝑇𝑤))
10		simpr 110	. . . . . 6 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → 𝐵 ∈ ℝ^)
11		3simpb 995	. . . . . 6 ⊢ ((𝑤 ∈ ℝ^* ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵) → (𝑤 ∈ ℝ^* ∧ 𝑤𝑆𝐵))
12		ixx.4	. . . . . . . 8 ⊢ ((𝑤 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝑤𝑆𝐵 → 𝑤𝑈𝐵))
13	12	ancoms 268	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) → (𝑤𝑆𝐵 → 𝑤𝑈𝐵))
14	13	expimpd 363	. . . . . 6 ⊢ (𝐵 ∈ ℝ^* → ((𝑤 ∈ ℝ^* ∧ 𝑤𝑆𝐵) → 𝑤𝑈𝐵))
15	10, 11, 14	syl2im 38	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → ((𝑤 ∈ ℝ^ ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵) → 𝑤𝑈𝐵))
16	4, 9, 15	3jcad 1178	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → ((𝑤 ∈ ℝ^ ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵) → (𝑤 ∈ ℝ^* ∧ 𝐴𝑇𝑤 ∧ 𝑤𝑈𝐵)))
17	1	elixx1 9899	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝑤 ∈ (𝐴𝑂𝐵) ↔ (𝑤 ∈ ℝ^ ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵)))
18		ixx.2	. . . . 5 ⊢ 𝑃 = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)})
19	18	elixx1 9899	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝑤 ∈ (𝐴𝑃𝐵) ↔ (𝑤 ∈ ℝ^ ∧ 𝐴𝑇𝑤 ∧ 𝑤𝑈𝐵)))
20	16, 17, 19	3imtr4d 203	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝑤 ∈ (𝐴𝑂𝐵) → 𝑤 ∈ (𝐴𝑃𝐵)))
21	2, 20	mpcom 36	. 2 ⊢ (𝑤 ∈ (𝐴𝑂𝐵) → 𝑤 ∈ (𝐴𝑃𝐵))
22	21	ssriv 3161	1 ⊢ (𝐴𝑂𝐵) ⊆ (𝐴𝑃𝐵)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 978 = wceq 1353 ∈ wcel 2148 {crab 2459 ⊆ wss 3131 class class class wbr 4005 (class class class)co 5877 ∈ cmpo 5879 ℝ^*cxr 7993

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-sep 4123 ax-pow 4176 ax-pr 4211 ax-un 4435 ax-setind 4538 ax-cnex 7904 ax-resscn 7905

This theorem depends on definitions: df-bi 117 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-ral 2460 df-rex 2461 df-rab 2464 df-v 2741 df-sbc 2965 df-dif 3133 df-un 3135 df-in 3137 df-ss 3144 df-pw 3579 df-sn 3600 df-pr 3601 df-op 3603 df-uni 3812 df-br 4006 df-opab 4067 df-id 4295 df-xp 4634 df-rel 4635 df-cnv 4636 df-co 4637 df-dm 4638 df-iota 5180 df-fun 5220 df-fv 5226 df-ov 5880 df-oprab 5881 df-mpo 5882 df-pnf 7996 df-mnf 7997 df-xr 7998

This theorem is referenced by: ioossicc 9961 icossicc 9962 iocssicc 9963 ioossico 9964

W3C validator