Mathbox for Zhi Wang |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > icccldii | Structured version Visualization version GIF version |
Description: Closed intervals are closed sets of II. Note that iccss 12861, iccordt 21929, and ordtresticc 21938 are proved from ixxss12 12813, ordtcld3 21914, and ordtrest2 21919, respectively. An alternate proof uses restcldi 21888, dfii2 23598, and icccld 23483. (Contributed by Zhi Wang, 8-Sep-2024.) |
Ref | Expression |
---|---|
icccldii | ⊢ ((0 ≤ 𝐴 ∧ 𝐵 ≤ 1) → (𝐴[,]𝐵) ∈ (Clsd‘II)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iccssxr 12876 | . . 3 ⊢ (0[,]1) ⊆ ℝ* | |
2 | iccordt 21929 | . . 3 ⊢ (𝐴[,]𝐵) ∈ (Clsd‘(ordTop‘ ≤ )) | |
3 | 0re 10695 | . . . 4 ⊢ 0 ∈ ℝ | |
4 | 1re 10693 | . . . 4 ⊢ 1 ∈ ℝ | |
5 | iccss 12861 | . . . 4 ⊢ (((0 ∈ ℝ ∧ 1 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≤ 1)) → (𝐴[,]𝐵) ⊆ (0[,]1)) | |
6 | 3, 4, 5 | mpanl12 701 | . . 3 ⊢ ((0 ≤ 𝐴 ∧ 𝐵 ≤ 1) → (𝐴[,]𝐵) ⊆ (0[,]1)) |
7 | letopuni 21922 | . . . 4 ⊢ ℝ* = ∪ (ordTop‘ ≤ ) | |
8 | 7 | restcldi 21888 | . . 3 ⊢ (((0[,]1) ⊆ ℝ* ∧ (𝐴[,]𝐵) ∈ (Clsd‘(ordTop‘ ≤ )) ∧ (𝐴[,]𝐵) ⊆ (0[,]1)) → (𝐴[,]𝐵) ∈ (Clsd‘((ordTop‘ ≤ ) ↾t (0[,]1)))) |
9 | 1, 2, 6, 8 | mp3an12i 1463 | . 2 ⊢ ((0 ≤ 𝐴 ∧ 𝐵 ≤ 1) → (𝐴[,]𝐵) ∈ (Clsd‘((ordTop‘ ≤ ) ↾t (0[,]1)))) |
10 | dfii5 23601 | . . . 4 ⊢ II = (ordTop‘( ≤ ∩ ((0[,]1) × (0[,]1)))) | |
11 | ordtresticc 21938 | . . . 4 ⊢ ((ordTop‘ ≤ ) ↾t (0[,]1)) = (ordTop‘( ≤ ∩ ((0[,]1) × (0[,]1)))) | |
12 | 10, 11 | eqtr4i 2785 | . . 3 ⊢ II = ((ordTop‘ ≤ ) ↾t (0[,]1)) |
13 | 12 | fveq2i 6667 | . 2 ⊢ (Clsd‘II) = (Clsd‘((ordTop‘ ≤ ) ↾t (0[,]1))) |
14 | 9, 13 | eleqtrrdi 2864 | 1 ⊢ ((0 ≤ 𝐴 ∧ 𝐵 ≤ 1) → (𝐴[,]𝐵) ∈ (Clsd‘II)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∈ wcel 2112 ∩ cin 3860 ⊆ wss 3861 class class class wbr 5037 × cxp 5527 ‘cfv 6341 (class class class)co 7157 ℝcr 10588 0cc0 10589 1c1 10590 ℝ*cxr 10726 ≤ cle 10728 [,]cicc 12796 ↾t crest 16767 ordTopcordt 16845 Clsdccld 21731 IIcii 23591 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2159 ax-12 2176 ax-ext 2730 ax-rep 5161 ax-sep 5174 ax-nul 5181 ax-pow 5239 ax-pr 5303 ax-un 7466 ax-cnex 10645 ax-resscn 10646 ax-1cn 10647 ax-icn 10648 ax-addcl 10649 ax-addrcl 10650 ax-mulcl 10651 ax-mulrcl 10652 ax-mulcom 10653 ax-addass 10654 ax-mulass 10655 ax-distr 10656 ax-i2m1 10657 ax-1ne0 10658 ax-1rid 10659 ax-rnegex 10660 ax-rrecex 10661 ax-cnre 10662 ax-pre-lttri 10663 ax-pre-lttrn 10664 ax-pre-ltadd 10665 ax-pre-mulgt0 10666 ax-pre-sup 10667 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2071 df-mo 2558 df-eu 2589 df-clab 2737 df-cleq 2751 df-clel 2831 df-nfc 2902 df-ne 2953 df-nel 3057 df-ral 3076 df-rex 3077 df-reu 3078 df-rmo 3079 df-rab 3080 df-v 3412 df-sbc 3700 df-csb 3809 df-dif 3864 df-un 3866 df-in 3868 df-ss 3878 df-pss 3880 df-nul 4229 df-if 4425 df-pw 4500 df-sn 4527 df-pr 4529 df-tp 4531 df-op 4533 df-uni 4803 df-int 4843 df-iun 4889 df-iin 4890 df-br 5038 df-opab 5100 df-mpt 5118 df-tr 5144 df-id 5435 df-eprel 5440 df-po 5448 df-so 5449 df-fr 5488 df-we 5490 df-xp 5535 df-rel 5536 df-cnv 5537 df-co 5538 df-dm 5539 df-rn 5540 df-res 5541 df-ima 5542 df-pred 6132 df-ord 6178 df-on 6179 df-lim 6180 df-suc 6181 df-iota 6300 df-fun 6343 df-fn 6344 df-f 6345 df-f1 6346 df-fo 6347 df-f1o 6348 df-fv 6349 df-riota 7115 df-ov 7160 df-oprab 7161 df-mpo 7162 df-om 7587 df-1st 7700 df-2nd 7701 df-wrecs 7964 df-recs 8025 df-rdg 8063 df-1o 8119 df-er 8306 df-map 8425 df-en 8542 df-dom 8543 df-sdom 8544 df-fin 8545 df-fi 8922 df-sup 8953 df-inf 8954 df-pnf 10729 df-mnf 10730 df-xr 10731 df-ltxr 10732 df-le 10733 df-sub 10924 df-neg 10925 df-div 11350 df-nn 11689 df-2 11751 df-3 11752 df-n0 11949 df-z 12035 df-uz 12297 df-q 12403 df-rp 12445 df-xneg 12562 df-xadd 12563 df-xmul 12564 df-ioo 12797 df-ioc 12798 df-ico 12799 df-icc 12800 df-seq 13433 df-exp 13494 df-cj 14520 df-re 14521 df-im 14522 df-sqrt 14656 df-abs 14657 df-rest 16769 df-topgen 16790 df-ordt 16847 df-ps 17891 df-tsr 17892 df-psmet 20173 df-xmet 20174 df-met 20175 df-bl 20176 df-mopn 20177 df-top 21609 df-topon 21626 df-bases 21661 df-cld 21734 df-ii 23593 |
This theorem is referenced by: sepfsepc 45673 seppcld 45675 |
Copyright terms: Public domain | W3C validator |