![]() |
Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > Mathboxes > xrstos | Structured version Unicode version |
Description: The extended real numbers form a toset. (Contributed by Thierry Arnoux, 15-Feb-2018.) |
Ref | Expression |
---|---|
xrstos |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xrsex 17951 |
. . 3
![]() ![]() ![]() ![]() ![]() | |
2 | xrleid 11233 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | ad2antrr 725 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | xrletri3 11235 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4 | biimprd 223 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | adantr 465 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | xrletr 11238 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 7 | 3expa 1188 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 3, 6, 8 | 3jca 1168 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 9 | ralrimiva 2827 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 10 | rgen2a 2894 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | xrsbas 17952 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
13 | xrsle 17956 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
14 | 12, 13 | ispos 15231 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 1, 11, 14 | mpbir2an 911 |
. 2
![]() ![]() ![]() ![]() ![]() |
16 | xrletri 11234 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
17 | 16 | rgen2a 2894 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
18 | 12, 13 | istos 15319 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
19 | 15, 17, 18 | mpbir2an 911 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1954 ax-ext 2431 ax-sep 4516 ax-nul 4524 ax-pow 4573 ax-pr 4634 ax-un 6477 ax-cnex 9444 ax-resscn 9445 ax-1cn 9446 ax-icn 9447 ax-addcl 9448 ax-addrcl 9449 ax-mulcl 9450 ax-mulrcl 9451 ax-mulcom 9452 ax-addass 9453 ax-mulass 9454 ax-distr 9455 ax-i2m1 9456 ax-1ne0 9457 ax-1rid 9458 ax-rnegex 9459 ax-rrecex 9460 ax-cnre 9461 ax-pre-lttri 9462 ax-pre-lttrn 9463 ax-pre-ltadd 9464 ax-pre-mulgt0 9465 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2265 df-mo 2266 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2602 df-ne 2647 df-nel 2648 df-ral 2801 df-rex 2802 df-reu 2803 df-rab 2805 df-v 3074 df-sbc 3289 df-csb 3391 df-dif 3434 df-un 3436 df-in 3438 df-ss 3445 df-pss 3447 df-nul 3741 df-if 3895 df-pw 3965 df-sn 3981 df-pr 3983 df-tp 3985 df-op 3987 df-uni 4195 df-int 4232 df-iun 4276 df-br 4396 df-opab 4454 df-mpt 4455 df-tr 4489 df-eprel 4735 df-id 4739 df-po 4744 df-so 4745 df-fr 4782 df-we 4784 df-ord 4825 df-on 4826 df-lim 4827 df-suc 4828 df-xp 4949 df-rel 4950 df-cnv 4951 df-co 4952 df-dm 4953 df-rn 4954 df-res 4955 df-ima 4956 df-iota 5484 df-fun 5523 df-fn 5524 df-f 5525 df-f1 5526 df-fo 5527 df-f1o 5528 df-fv 5529 df-riota 6156 df-ov 6198 df-oprab 6199 df-mpt2 6200 df-om 6582 df-1st 6682 df-2nd 6683 df-recs 6937 df-rdg 6971 df-1o 7025 df-oadd 7029 df-er 7206 df-en 7416 df-dom 7417 df-sdom 7418 df-fin 7419 df-pnf 9526 df-mnf 9527 df-xr 9528 df-ltxr 9529 df-le 9530 df-sub 9703 df-neg 9704 df-nn 10429 df-2 10486 df-3 10487 df-4 10488 df-5 10489 df-6 10490 df-7 10491 df-8 10492 df-9 10493 df-10 10494 df-n0 10686 df-z 10753 df-dec 10862 df-uz 10968 df-fz 11550 df-struct 14289 df-ndx 14290 df-slot 14291 df-base 14292 df-plusg 14365 df-mulr 14366 df-tset 14371 df-ple 14372 df-ds 14374 df-xrs 14554 df-poset 15230 df-toset 15318 |
This theorem is referenced by: xrsclat 26281 xrsp0 26282 xrsp1 26283 |
Copyright terms: Public domain | W3C validator |