![]() |
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 5150 | . . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑦𝐴𝑧 → 𝑦𝐵𝑧)) | |
2 | 1 | anim2d 613 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥𝐶𝑦 ∧ 𝑦𝐴𝑧) → (𝑥𝐶𝑦 ∧ 𝑦𝐵𝑧))) |
3 | 2 | eximdv 1921 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐴𝑧) → ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐵𝑧))) |
4 | 3 | ssopab2dv 5509 | . 2 ⊢ (𝐴 ⊆ 𝐵 → {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐴𝑧)} ⊆ {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐵𝑧)}) |
5 | df-co 5643 | . 2 ⊢ (𝐴 ∘ 𝐶) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐴𝑧)} | |
6 | df-co 5643 | . 2 ⊢ (𝐵 ∘ 𝐶) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐵𝑧)} | |
7 | 4, 5, 6 | 3sstr4g 3990 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∃wex 1782 ⊆ wss 3911 class class class wbr 5106 {copab 5168 ∘ ccom 5638 |
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 3446 df-in 3918 df-ss 3928 df-br 5107 df-opab 5169 df-co 5643 |
This theorem is referenced by: coeq1 5814 funss 6521 tposss 8159 cottrcl 9660 frmin 9690 frrlem16 9699 rtrclreclem4 14952 tsrdir 18498 ustex2sym 23584 ustex3sym 23585 ustneism 23591 trust 23597 utop2nei 23618 neipcfilu 23664 trclubgNEW 41978 trrelsuperrel2dg 42031 trclrelexplem 42071 cotrcltrcl 42085 cotrclrcl 42102 frege96d 42109 frege97d 42112 frege109d 42117 frege131d 42124 |
Copyright terms: Public domain | W3C validator |