ixxssixx - Intuitionistic Logic Explorer

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

Theorem ixxssixx 9575

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 5922	. . 3 ⊢ (𝑤 ∈ (𝐴𝑂𝐵) → (𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*))
3		simp1 964	. . . . . 6 ⊢ ((𝑤 ∈ ℝ^* ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵) → 𝑤 ∈ ℝ^*)
4	3	a1i 9	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → ((𝑤 ∈ ℝ^ ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵) → 𝑤 ∈ ℝ^*))
5		simpl 108	. . . . . 6 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → 𝐴 ∈ ℝ^)
6		3simpa 961	. . . . . 6 ⊢ ((𝑤 ∈ ℝ^* ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵) → (𝑤 ∈ ℝ^* ∧ 𝐴𝑅𝑤))
7		ixx.3	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) → (𝐴𝑅𝑤 → 𝐴𝑇𝑤))
8	7	expimpd 358	. . . . . 6 ⊢ (𝐴 ∈ ℝ^* → ((𝑤 ∈ ℝ^* ∧ 𝐴𝑅𝑤) → 𝐴𝑇𝑤))
9	5, 6, 8	syl2im 38	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → ((𝑤 ∈ ℝ^ ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵) → 𝐴𝑇𝑤))
10		simpr 109	. . . . . 6 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → 𝐵 ∈ ℝ^)
11		3simpb 962	. . . . . 6 ⊢ ((𝑤 ∈ ℝ^* ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵) → (𝑤 ∈ ℝ^* ∧ 𝑤𝑆𝐵))
12		ixx.4	. . . . . . . 8 ⊢ ((𝑤 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝑤𝑆𝐵 → 𝑤𝑈𝐵))
13	12	ancoms 266	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) → (𝑤𝑆𝐵 → 𝑤𝑈𝐵))
14	13	expimpd 358	. . . . . 6 ⊢ (𝐵 ∈ ℝ^* → ((𝑤 ∈ ℝ^* ∧ 𝑤𝑆𝐵) → 𝑤𝑈𝐵))
15	10, 11, 14	syl2im 38	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → ((𝑤 ∈ ℝ^ ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵) → 𝑤𝑈𝐵))
16	4, 9, 15	3jcad 1145	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → ((𝑤 ∈ ℝ^ ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵) → (𝑤 ∈ ℝ^* ∧ 𝐴𝑇𝑤 ∧ 𝑤𝑈𝐵)))
17	1	elixx1 9570	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝑤 ∈ (𝐴𝑂𝐵) ↔ (𝑤 ∈ ℝ^ ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵)))
18		ixx.2	. . . . 5 ⊢ 𝑃 = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)})
19	18	elixx1 9570	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝑤 ∈ (𝐴𝑃𝐵) ↔ (𝑤 ∈ ℝ^ ∧ 𝐴𝑇𝑤 ∧ 𝑤𝑈𝐵)))
20	16, 17, 19	3imtr4d 202	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝑤 ∈ (𝐴𝑂𝐵) → 𝑤 ∈ (𝐴𝑃𝐵)))
21	2, 20	mpcom 36	. 2 ⊢ (𝑤 ∈ (𝐴𝑂𝐵) → 𝑤 ∈ (𝐴𝑃𝐵))
22	21	ssriv 3067	1 ⊢ (𝐴𝑂𝐵) ⊆ (𝐴𝑃𝐵)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 945 = wceq 1314 ∈ wcel 1463 {crab 2394 ⊆ wss 3037 class class class wbr 3895 (class class class)co 5728 ∈ cmpo 5730 ℝ^*cxr 7720

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 586 ax-in2 587 ax-io 681 ax-5 1406 ax-7 1407 ax-gen 1408 ax-ie1 1452 ax-ie2 1453 ax-8 1465 ax-10 1466 ax-11 1467 ax-i12 1468 ax-bndl 1469 ax-4 1470 ax-13 1474 ax-14 1475 ax-17 1489 ax-i9 1493 ax-ial 1497 ax-i5r 1498 ax-ext 2097 ax-sep 4006 ax-pow 4058 ax-pr 4091 ax-un 4315 ax-setind 4412 ax-cnex 7633 ax-resscn 7634

This theorem depends on definitions: df-bi 116 df-3an 947 df-tru 1317 df-fal 1320 df-nf 1420 df-sb 1719 df-eu 1978 df-mo 1979 df-clab 2102 df-cleq 2108 df-clel 2111 df-nfc 2244 df-ne 2283 df-ral 2395 df-rex 2396 df-rab 2399 df-v 2659 df-sbc 2879 df-dif 3039 df-un 3041 df-in 3043 df-ss 3050 df-pw 3478 df-sn 3499 df-pr 3500 df-op 3502 df-uni 3703 df-br 3896 df-opab 3950 df-id 4175 df-xp 4505 df-rel 4506 df-cnv 4507 df-co 4508 df-dm 4509 df-iota 5046 df-fun 5083 df-fv 5089 df-ov 5731 df-oprab 5732 df-mpo 5733 df-pnf 7723 df-mnf 7724 df-xr 7725

This theorem is referenced by: ioossicc 9632 icossicc 9633 iocssicc 9634 ioossico 9635

W3C validator