![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > coss1 | Structured version Visualization version GIF version |
Description: Subclass theorem for composition. (Contributed by FL, 30-Dec-2010.) |
Ref | Expression |
---|---|
coss1 | ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssbr 5193 | . . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑦𝐴𝑧 → 𝑦𝐵𝑧)) | |
2 | 1 | anim2d 613 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥𝐶𝑦 ∧ 𝑦𝐴𝑧) → (𝑥𝐶𝑦 ∧ 𝑦𝐵𝑧))) |
3 | 2 | eximdv 1921 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐴𝑧) → ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐵𝑧))) |
4 | 3 | ssopab2dv 5552 | . 2 ⊢ (𝐴 ⊆ 𝐵 → {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐴𝑧)} ⊆ {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐵𝑧)}) |
5 | df-co 5686 | . 2 ⊢ (𝐴 ∘ 𝐶) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐴𝑧)} | |
6 | df-co 5686 | . 2 ⊢ (𝐵 ∘ 𝐶) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐵𝑧)} | |
7 | 4, 5, 6 | 3sstr4g 4028 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∃wex 1782 ⊆ wss 3949 class class class wbr 5149 {copab 5211 ∘ ccom 5681 |
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 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-in 3956 df-ss 3966 df-br 5150 df-opab 5212 df-co 5686 |
This theorem is referenced by: coeq1 5858 funss 6568 tposss 8212 cottrcl 9714 frmin 9744 frrlem16 9753 rtrclreclem4 15008 tsrdir 18557 ustex2sym 23721 ustex3sym 23722 ustneism 23728 trust 23734 utop2nei 23755 neipcfilu 23801 trclubgNEW 42369 trrelsuperrel2dg 42422 trclrelexplem 42462 cotrcltrcl 42476 cotrclrcl 42493 frege96d 42500 frege97d 42503 frege109d 42508 frege131d 42515 |
Copyright terms: Public domain | W3C validator |