Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > elxr | GIF version |
Description: Membership in the set of extended reals. (Contributed by NM, 14-Oct-2005.) |
Ref | Expression |
---|---|
elxr | ⊢ (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-xr 7928 | . . 3 ⊢ ℝ* = (ℝ ∪ {+∞, -∞}) | |
2 | 1 | eleq2i 2231 | . 2 ⊢ (𝐴 ∈ ℝ* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞})) |
3 | elun 3258 | . 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞})) | |
4 | pnfex 7943 | . . . . 5 ⊢ +∞ ∈ V | |
5 | mnfxr 7946 | . . . . . 6 ⊢ -∞ ∈ ℝ* | |
6 | 5 | elexi 2733 | . . . . 5 ⊢ -∞ ∈ V |
7 | 4, 6 | elpr2 3592 | . . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞)) |
8 | 7 | orbi2i 752 | . . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞))) |
9 | 3orass 970 | . . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞))) | |
10 | 8, 9 | bitr4i 186 | . 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞)) |
11 | 2, 3, 10 | 3bitri 205 | 1 ⊢ (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞)) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ∨ wo 698 ∨ w3o 966 = wceq 1342 ∈ wcel 2135 ∪ cun 3109 {cpr 3571 ℝcr 7743 +∞cpnf 7921 -∞cmnf 7922 ℝ*cxr 7923 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-13 2137 ax-14 2138 ax-ext 2146 ax-sep 4094 ax-pow 4147 ax-un 4405 ax-cnex 7835 |
This theorem depends on definitions: df-bi 116 df-3or 968 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-rex 2448 df-v 2723 df-un 3115 df-in 3117 df-ss 3124 df-pw 3555 df-sn 3576 df-pr 3577 df-uni 3784 df-pnf 7926 df-mnf 7927 df-xr 7928 |
This theorem is referenced by: xrnemnf 9704 xrnepnf 9705 xrltnr 9706 xrltnsym 9720 xrlttr 9722 xrltso 9723 xrlttri3 9724 nltpnft 9741 npnflt 9742 ngtmnft 9744 nmnfgt 9745 xrrebnd 9746 xnegcl 9759 xnegneg 9760 xltnegi 9762 xrpnfdc 9769 xrmnfdc 9770 xnegid 9786 xaddcom 9788 xaddid1 9789 xnegdi 9795 xleadd1a 9800 xltadd1 9803 xlt2add 9807 xsubge0 9808 xposdif 9809 xleaddadd 9814 qbtwnxr 10183 xrmaxiflemcl 11172 xrmaxifle 11173 xrmaxiflemab 11174 xrmaxiflemlub 11175 xrmaxltsup 11185 xrmaxadd 11188 xrbdtri 11203 isxmet2d 12889 blssioo 13086 |
Copyright terms: Public domain | W3C validator |