ixxssixx - Intuitionistic Logic Explorer

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

Theorem ixxssixx 10044

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 6154	. . 3 ⊢ (𝑤 ∈ (𝐴𝑂𝐵) → (𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*))
3		simp1 1000	. . . . . 6 ⊢ ((𝑤 ∈ ℝ^* ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵) → 𝑤 ∈ ℝ^*)
4	3	a1i 9	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → ((𝑤 ∈ ℝ^ ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵) → 𝑤 ∈ ℝ^*))
5		simpl 109	. . . . . 6 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → 𝐴 ∈ ℝ^)
6		3simpa 997	. . . . . 6 ⊢ ((𝑤 ∈ ℝ^* ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵) → (𝑤 ∈ ℝ^* ∧ 𝐴𝑅𝑤))
7		ixx.3	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) → (𝐴𝑅𝑤 → 𝐴𝑇𝑤))
8	7	expimpd 363	. . . . . 6 ⊢ (𝐴 ∈ ℝ^* → ((𝑤 ∈ ℝ^* ∧ 𝐴𝑅𝑤) → 𝐴𝑇𝑤))
9	5, 6, 8	syl2im 38	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → ((𝑤 ∈ ℝ^ ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵) → 𝐴𝑇𝑤))
10		simpr 110	. . . . . 6 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → 𝐵 ∈ ℝ^)
11		3simpb 998	. . . . . 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 1181	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → ((𝑤 ∈ ℝ^ ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵) → (𝑤 ∈ ℝ^* ∧ 𝐴𝑇𝑤 ∧ 𝑤𝑈𝐵)))
17	1	elixx1 10039	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝑤 ∈ (𝐴𝑂𝐵) ↔ (𝑤 ∈ ℝ^ ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵)))
18		ixx.2	. . . . 5 ⊢ 𝑃 = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)})
19	18	elixx1 10039	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝑤 ∈ (𝐴𝑃𝐵) ↔ (𝑤 ∈ ℝ^ ∧ 𝐴𝑇𝑤 ∧ 𝑤𝑈𝐵)))
20	16, 17, 19	3imtr4d 203	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝑤 ∈ (𝐴𝑂𝐵) → 𝑤 ∈ (𝐴𝑃𝐵)))
21	2, 20	mpcom 36	. 2 ⊢ (𝑤 ∈ (𝐴𝑂𝐵) → 𝑤 ∈ (𝐴𝑃𝐵))
22	21	ssriv 3201	1 ⊢ (𝐴𝑂𝐵) ⊆ (𝐴𝑃𝐵)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 981 = wceq 1373 ∈ wcel 2177 {crab 2489 ⊆ wss 3170 class class class wbr 4051 (class class class)co 5957 ∈ cmpo 5959 ℝ^*cxr 8126

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 615 ax-in2 616 ax-io 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-sep 4170 ax-pow 4226 ax-pr 4261 ax-un 4488 ax-setind 4593 ax-cnex 8036 ax-resscn 8037

This theorem depends on definitions: df-bi 117 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ne 2378 df-ral 2490 df-rex 2491 df-rab 2494 df-v 2775 df-sbc 3003 df-dif 3172 df-un 3174 df-in 3176 df-ss 3183 df-pw 3623 df-sn 3644 df-pr 3645 df-op 3647 df-uni 3857 df-br 4052 df-opab 4114 df-id 4348 df-xp 4689 df-rel 4690 df-cnv 4691 df-co 4692 df-dm 4693 df-iota 5241 df-fun 5282 df-fv 5288 df-ov 5960 df-oprab 5961 df-mpo 5962 df-pnf 8129 df-mnf 8130 df-xr 8131

This theorem is referenced by: ioossicc 10101 icossicc 10102 iocssicc 10103 ioossico 10104

W3C validator