![]() |
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 5548 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Po 𝐵 → 𝑅 Po 𝐴)) | |
2 | ss2ralv 4013 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) | |
3 | 1, 2 | anim12d 610 | . 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) → (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))) |
4 | df-so 5547 | . 2 ⊢ (𝑅 Or 𝐵 ↔ (𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) | |
5 | df-so 5547 | . 2 ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) | |
6 | 3, 4, 5 | 3imtr4g 296 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Or 𝐵 → 𝑅 Or 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∨ w3o 1087 ∀wral 3065 ⊆ wss 3911 class class class wbr 5106 Po wpo 5544 Or wor 5545 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-ral 3066 df-v 3448 df-in 3918 df-ss 3928 df-po 5546 df-so 5547 |
This theorem is referenced by: soeq2 5568 wess 5621 wereu 5630 wereu2 5631 ordunifi 9238 fisup2g 9405 fisupcl 9406 fiinf2g 9437 ordtypelem8 9462 wemapso2lem 9489 iunfictbso 10051 fin1a2lem10 10346 fin1a2lem11 10347 zornn0g 10442 ltsopi 10825 npomex 10933 fimaxre 12100 fiminre 12103 suprfinzcl 12618 isercolllem1 15550 summolem2 15602 zsum 15604 prodmolem2 15819 zprod 15821 gsumval3 19685 iccpnfhmeo 24311 xrhmeo 24312 dvgt0lem2 25370 dgrval 25592 dgrcl 25597 dgrub 25598 dgrlb 25600 aannenlem3 25693 logccv 26021 nomaxmo 27049 nominmo 27050 xrge0infssd 31669 infxrge0lb 31672 infxrge0glb 31673 infxrge0gelb 31674 ssnnssfz 31693 xrge0iifiso 32519 omsfval 32897 omsf 32899 oms0 32900 omssubaddlem 32902 omssubadd 32903 oddpwdc 32957 erdszelem4 33791 erdszelem8 33795 erdsze2lem1 33800 erdsze2lem2 33801 supfz 34304 inffz 34305 finorwe 35856 fin2so 36068 sticksstones3 40559 rencldnfilem 41146 fzisoeu 43541 fourierdlem36 44391 ssnn0ssfz 46432 |
Copyright terms: Public domain | W3C validator |