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 5101 | . . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑦𝐴𝑧 → 𝑦𝐵𝑧)) | |
2 | 1 | anim2d 611 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥𝐶𝑦 ∧ 𝑦𝐴𝑧) → (𝑥𝐶𝑦 ∧ 𝑦𝐵𝑧))) |
3 | 2 | eximdv 1909 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐴𝑧) → ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐵𝑧))) |
4 | 3 | ssopab2dv 5429 | . 2 ⊢ (𝐴 ⊆ 𝐵 → {〈𝑥, 𝑧〉 ∣ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐴𝑧)} ⊆ {〈𝑥, 𝑧〉 ∣ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐵𝑧)}) |
5 | df-co 5557 | . 2 ⊢ (𝐴 ∘ 𝐶) = {〈𝑥, 𝑧〉 ∣ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐴𝑧)} | |
6 | df-co 5557 | . 2 ⊢ (𝐵 ∘ 𝐶) = {〈𝑥, 𝑧〉 ∣ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐵𝑧)} | |
7 | 4, 5, 6 | 3sstr4g 4009 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∃wex 1771 ⊆ wss 3933 class class class wbr 5057 {copab 5119 ∘ ccom 5552 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-in 3940 df-ss 3949 df-br 5058 df-opab 5120 df-co 5557 |
This theorem is referenced by: coeq1 5721 funss 6367 tposss 7882 rtrclreclem4 14408 tsrdir 17836 ustex2sym 22752 ustex3sym 22753 ustneism 22759 trust 22765 utop2nei 22786 neipcfilu 22832 trclubgNEW 39856 trrelsuperrel2dg 39894 trclrelexplem 39934 cotrcltrcl 39948 cotrclrcl 39965 frege96d 39972 frege97d 39975 frege109d 39980 frege131d 39987 |
Copyright terms: Public domain | W3C validator |