| 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 5594 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Po 𝐵 → 𝑅 Po 𝐴)) | |
| 2 | ss2ralv 4054 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) | |
| 3 | 1, 2 | anim12d 609 | . 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) → (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))) |
| 4 | df-so 5593 | . 2 ⊢ (𝑅 Or 𝐵 ↔ (𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) | |
| 5 | df-so 5593 | . 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 1086 ∀wral 3061 ⊆ wss 3951 class class class wbr 5143 Po wpo 5590 Or wor 5591 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ral 3062 df-ss 3968 df-po 5592 df-so 5593 |
| This theorem is referenced by: soeq2 5614 wess 5671 wereu 5681 wereu2 5682 ordunifi 9326 fisup2g 9508 fisupcl 9509 fiinf2g 9540 ordtypelem8 9565 wemapso2lem 9592 iunfictbso 10154 fin1a2lem10 10449 fin1a2lem11 10450 zornn0g 10545 ltsopi 10928 npomex 11036 fimaxre 12212 fiminre 12215 suprfinzcl 12732 isercolllem1 15701 summolem2 15752 zsum 15754 prodmolem2 15971 zprod 15973 gsumval3 19925 iccpnfhmeo 24976 xrhmeo 24977 dvgt0lem2 26042 dgrval 26267 dgrcl 26272 dgrub 26273 dgrlb 26275 aannenlem3 26372 logccv 26705 nomaxmo 27743 nominmo 27744 xrge0infssd 32765 infxrge0lb 32768 infxrge0glb 32769 infxrge0gelb 32770 ssnnssfz 32789 xrge0iifiso 33934 omsfval 34296 omsf 34298 oms0 34299 omssubaddlem 34301 omssubadd 34302 oddpwdc 34356 erdszelem4 35199 erdszelem8 35203 erdsze2lem1 35208 erdsze2lem2 35209 supfz 35729 inffz 35730 finorwe 37383 fin2so 37614 sticksstones3 42149 rencldnfilem 42831 fzisoeu 45312 fourierdlem36 46158 ssnn0ssfz 48265 |
| Copyright terms: Public domain | W3C validator |