Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > soss | Structured version Visualization version Unicode version |
Description: Subset theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Ref | Expression |
---|---|
soss |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | poss 5037 | . . 3 | |
2 | ssel 3597 | . . . . . . 7 | |
3 | ssel 3597 | . . . . . . 7 | |
4 | 2, 3 | anim12d 586 | . . . . . 6 |
5 | 4 | imim1d 82 | . . . . 5 |
6 | 5 | 2alimdv 1847 | . . . 4 |
7 | r2al 2939 | . . . 4 | |
8 | r2al 2939 | . . . 4 | |
9 | 6, 7, 8 | 3imtr4g 285 | . . 3 |
10 | 1, 9 | anim12d 586 | . 2 |
11 | df-so 5036 | . 2 | |
12 | df-so 5036 | . 2 | |
13 | 10, 11, 12 | 3imtr4g 285 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 w3o 1036 wal 1481 wcel 1990 wral 2912 wss 3574 class class class wbr 4653 wpo 5033 wor 5034 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-ral 2917 df-in 3581 df-ss 3588 df-po 5035 df-so 5036 |
This theorem is referenced by: soeq2 5055 wess 5101 wereu 5110 wereu2 5111 ordunifi 8210 fisup2g 8374 fisupcl 8375 fiinf2g 8406 ordtypelem8 8430 wemapso2lem 8457 iunfictbso 8937 fin1a2lem10 9231 fin1a2lem11 9232 zornn0g 9327 ltsopi 9710 npomex 9818 fimaxre 10968 suprfinzcl 11492 isercolllem1 14395 summolem2 14447 zsum 14449 prodmolem2 14665 zprod 14667 gsumval3 18308 iccpnfhmeo 22744 xrhmeo 22745 dvgt0lem2 23766 dgrval 23984 dgrcl 23989 dgrub 23990 dgrlb 23992 aannenlem3 24085 logccv 24409 xrge0infssd 29526 infxrge0lb 29529 infxrge0glb 29530 infxrge0gelb 29531 ssnnssfz 29549 xrge0iifiso 29981 omsfval 30356 omsf 30358 oms0 30359 omssubaddlem 30361 omssubadd 30362 oddpwdc 30416 erdszelem4 31176 erdszelem8 31180 erdsze2lem1 31185 erdsze2lem2 31186 supfz 31613 inffz 31614 inffzOLD 31615 nomaxmo 31847 fin2so 33396 rencldnfilem 37384 fzisoeu 39514 fourierdlem36 40360 ssnn0ssfz 42127 |
Copyright terms: Public domain | W3C validator |