![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > coss2 | Structured version Visualization version GIF version |
Description: Subclass theorem for composition. (Contributed by NM, 5-Apr-2013.) |
Ref | Expression |
---|---|
coss2 | ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssbr 5150 | . . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑥𝐴𝑦 → 𝑥𝐵𝑦)) | |
2 | 1 | anim1d 612 | . . . 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: coeq2 5815 funss 6521 tposss 8159 dftpos4 8177 ttrclco 9659 frmin 9690 frrlem16 9699 rtrclreclem4 14952 tsrdir 18498 mvdco 19232 ustex2sym 23584 ustex3sym 23585 ustneism 23591 trust 23597 utop2nei 23618 neipcfilu 23664 fcoinver 31571 trclubgNEW 41978 trrelsuperrel2dg 42031 |
Copyright terms: Public domain | W3C validator |