snunioo - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > snunioo		Structured version Visualization version GIF version

Theorem snunioo 13524

Description: The closure of one end of an open real interval. (Contributed by Paul Chapman, 15-Mar-2008.) (Proof shortened by Mario Carneiro, 16-Jun-2014.)

**Assertion**
Ref	Expression
snunioo	⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) → ({𝐴} ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵))

Proof of Theorem snunioo Dummy variables 𝑥 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp1 1137	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) → 𝐴 ∈ ℝ^*)
2		iccid 13438	. . . 4 ⊢ (𝐴 ∈ ℝ^* → (𝐴[,]𝐴) = {𝐴})
3	1, 2	syl 17	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) → (𝐴[,]𝐴) = {𝐴})
4	3	uneq1d 4180	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) → ((𝐴[,]𝐴) ∪ (𝐴(,)𝐵)) = ({𝐴} ∪ (𝐴(,)𝐵)))
5		simp2 1138	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℝ^*)
6	1	xrleidd 13200	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) → 𝐴 ≤ 𝐴)
7		simp3 1139	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) → 𝐴 < 𝐵)
8		df-icc 13400	. . . 4 ⊢ [,] = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})
9		df-ioo 13397	. . . 4 ⊢ (,) = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
10		xrltnle 11335	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) → (𝐴 < 𝑤 ↔ ¬ 𝑤 ≤ 𝐴))
11		df-ico 13399	. . . 4 ⊢ [,) = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
12		xrlelttr 13204	. . . 4 ⊢ ((𝑤 ∈ ℝ^* ∧ 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → ((𝑤 ≤ 𝐴 ∧ 𝐴 < 𝐵) → 𝑤 < 𝐵))
13		xrltle 13197	. . . . . 6 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) → (𝐴 < 𝑤 → 𝐴 ≤ 𝑤))
14	13	3adant1 1131	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) → (𝐴 < 𝑤 → 𝐴 ≤ 𝑤))
15	14	adantld 490	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) → ((𝐴 ≤ 𝐴 ∧ 𝐴 < 𝑤) → 𝐴 ≤ 𝑤))
16	8, 9, 10, 11, 12, 15	ixxun 13409	. . 3 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → ((𝐴[,]𝐴) ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵))
17	1, 1, 5, 6, 7, 16	syl32anc 1379	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) → ((𝐴[,]𝐴) ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵))
18	4, 17	eqtr3d 2779	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) → ({𝐴} ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ w3a 1087 = wceq 1539 ∈ wcel 2108 ∪ cun 3964 {csn 4634 class class class wbr 5151 (class class class)co 7438 ℝ^*cxr 11301 < clt 11302 ≤ cle 11303 (,)cioo 13393 [,)cico 13395 [,]cicc 13396

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5305 ax-nul 5315 ax-pow 5374 ax-pr 5441 ax-un 7761 ax-cnex 11218 ax-resscn 11219 ax-pre-lttri 11236 ax-pre-lttrn 11237

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3483 df-sbc 3795 df-csb 3912 df-dif 3969 df-un 3971 df-in 3973 df-ss 3983 df-nul 4343 df-if 4535 df-pw 4610 df-sn 4635 df-pr 4637 df-op 4641 df-uni 4916 df-br 5152 df-opab 5214 df-mpt 5235 df-id 5587 df-po 5601 df-so 5602 df-xp 5699 df-rel 5700 df-cnv 5701 df-co 5702 df-dm 5703 df-rn 5704 df-res 5705 df-ima 5706 df-iota 6522 df-fun 6571 df-fn 6572 df-f 6573 df-f1 6574 df-fo 6575 df-f1o 6576 df-fv 6577 df-ov 7441 df-oprab 7442 df-mpo 7443 df-er 8753 df-en 8994 df-dom 8995 df-sdom 8996 df-pnf 11304 df-mnf 11305 df-xr 11306 df-ltxr 11307 df-le 11308 df-ioo 13397 df-ico 13399 df-icc 13400

This theorem is referenced by: prunioo 13527 ioojoin 13529 icombl1 25623 ioombl 25625 tan2h 37613 mbfposadd 37668 itg2addnclem2 37673 ftc1anclem5 37698 iocunico 43216 limciccioolb 45605 fourierdlem32 46123 fourierdlem93 46183

W3C validator