![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > soss | Structured version Visualization version GIF 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 | ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Or 𝐵 → 𝑅 Or 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | poss 5587 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Po 𝐵 → 𝑅 Po 𝐴)) | |
2 | ss2ralv 4049 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) | |
3 | 1, 2 | anim12d 608 | . 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) → (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))) |
4 | df-so 5586 | . 2 ⊢ (𝑅 Or 𝐵 ↔ (𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) | |
5 | df-so 5586 | . 2 ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) | |
6 | 3, 4, 5 | 3imtr4g 296 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Or 𝐵 → 𝑅 Or 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∨ w3o 1084 ∀wral 3057 ⊆ wss 3945 class class class wbr 5143 Po wpo 5583 Or wor 5584 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-ral 3058 df-v 3472 df-in 3952 df-ss 3962 df-po 5585 df-so 5586 |
This theorem is referenced by: soeq2 5607 wess 5660 wereu 5669 wereu2 5670 ordunifi 9312 fisup2g 9486 fisupcl 9487 fiinf2g 9518 ordtypelem8 9543 wemapso2lem 9570 iunfictbso 10132 fin1a2lem10 10427 fin1a2lem11 10428 zornn0g 10523 ltsopi 10906 npomex 11014 fimaxre 12183 fiminre 12186 suprfinzcl 12701 isercolllem1 15638 summolem2 15689 zsum 15691 prodmolem2 15906 zprod 15908 gsumval3 19856 iccpnfhmeo 24864 xrhmeo 24865 dvgt0lem2 25930 dgrval 26156 dgrcl 26161 dgrub 26162 dgrlb 26164 aannenlem3 26259 logccv 26591 nomaxmo 27625 nominmo 27626 xrge0infssd 32526 infxrge0lb 32529 infxrge0glb 32530 infxrge0gelb 32531 ssnnssfz 32550 xrge0iifiso 33531 omsfval 33909 omsf 33911 oms0 33912 omssubaddlem 33914 omssubadd 33915 oddpwdc 33969 erdszelem4 34799 erdszelem8 34803 erdsze2lem1 34808 erdsze2lem2 34809 supfz 35318 inffz 35319 finorwe 36856 fin2so 37075 sticksstones3 41615 rencldnfilem 42231 fzisoeu 44673 fourierdlem36 45522 ssnn0ssfz 47404 |
Copyright terms: Public domain | W3C validator |