![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > xrletrid | Structured version Visualization version GIF version |
Description: Trichotomy law for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Ref | Expression |
---|---|
xrletrid.1 | ⊢ (𝜑 → 𝐴 ∈ ℝ*) |
xrletrid.2 | ⊢ (𝜑 → 𝐵 ∈ ℝ*) |
xrletrid.3 | ⊢ (𝜑 → 𝐴 ≤ 𝐵) |
xrletrid.4 | ⊢ (𝜑 → 𝐵 ≤ 𝐴) |
Ref | Expression |
---|---|
xrletrid | ⊢ (𝜑 → 𝐴 = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xrletrid.3 | . 2 ⊢ (𝜑 → 𝐴 ≤ 𝐵) | |
2 | xrletrid.4 | . 2 ⊢ (𝜑 → 𝐵 ≤ 𝐴) | |
3 | xrletrid.1 | . . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ*) | |
4 | xrletrid.2 | . . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ*) | |
5 | xrletri3 12357 | . . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) | |
6 | 3, 4, 5 | syl2anc 576 | . 2 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
7 | 1, 2, 6 | mpbir2and 700 | 1 ⊢ (𝜑 → 𝐴 = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 = wceq 1507 ∈ wcel 2048 class class class wbr 4923 ℝ*cxr 10465 ≤ cle 10467 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-13 2299 ax-ext 2745 ax-sep 5054 ax-nul 5061 ax-pow 5113 ax-pr 5180 ax-un 7273 ax-cnex 10383 ax-resscn 10384 ax-pre-lttri 10401 ax-pre-lttrn 10402 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2014 df-mo 2544 df-eu 2580 df-clab 2754 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-nel 3068 df-ral 3087 df-rex 3088 df-rab 3091 df-v 3411 df-sbc 3678 df-csb 3783 df-dif 3828 df-un 3830 df-in 3832 df-ss 3839 df-nul 4174 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4707 df-br 4924 df-opab 4986 df-mpt 5003 df-id 5305 df-po 5319 df-so 5320 df-xp 5406 df-rel 5407 df-cnv 5408 df-co 5409 df-dm 5410 df-rn 5411 df-res 5412 df-ima 5413 df-iota 6146 df-fun 6184 df-fn 6185 df-f 6186 df-f1 6187 df-fo 6188 df-f1o 6189 df-fv 6190 df-er 8081 df-en 8299 df-dom 8300 df-sdom 8301 df-pnf 10468 df-mnf 10469 df-xr 10470 df-ltxr 10471 df-le 10472 |
This theorem is referenced by: supxrre 12529 infxrre 12538 ixxub 12568 ixxlb 12569 pcadd2 16072 psmetsym 22613 xmetsym 22650 imasdsf1olem 22676 ovolunnul 23794 ovolicc 23817 voliunlem3 23846 uniioovol 23873 uniiccvol 23874 ismbfd 23933 mbflimsup 23960 itg2itg1 24030 itg2seq 24036 itg2eqa 24039 itg2split 24043 itg2mono 24047 deg1add 24390 deg1mul2 24401 deg1tm 24405 xrgepnfd 40974 supxrge 40981 infxrpnf 41098 eliccnelico 41182 liminfgelimsup 41440 liminfgelimsupuz 41446 liminflimsupclim 41465 xlimliminflimsup 41520 ismbl4 41655 rrxsnicc 41962 sge0fsum 42046 sge0split 42068 sge0iunmptlemre 42074 sge0isum 42086 sge0xaddlem2 42093 sge0reuz 42106 meale0eq0 42137 carageniuncl 42182 caratheodorylem2 42186 caragenel2d 42191 omess0 42193 ovn0lem 42224 hoidmv1lelem2 42251 hoidmv1lelem3 42252 hoidmvlelem4 42257 ovnhoi 42262 ovolval2lem 42302 ovolval5lem3 42313 |
Copyright terms: Public domain | W3C validator |