![]() |
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 5149 | . . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑥𝐴𝑦 → 𝑥𝐵𝑦)) | |
2 | 1 | anim1d 611 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥𝐴𝑦 ∧ 𝑦𝐶𝑧) → (𝑥𝐵𝑦 ∧ 𝑦𝐶𝑧))) |
3 | 2 | eximdv 1920 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥𝐴𝑦 ∧ 𝑦𝐶𝑧) → ∃𝑦(𝑥𝐵𝑦 ∧ 𝑦𝐶𝑧))) |
4 | 3 | ssopab2dv 5508 | . 2 ⊢ (𝐴 ⊆ 𝐵 → {〈𝑥, 𝑧〉 ∣ ∃𝑦(𝑥𝐴𝑦 ∧ 𝑦𝐶𝑧)} ⊆ {〈𝑥, 𝑧〉 ∣ ∃𝑦(𝑥𝐵𝑦 ∧ 𝑦𝐶𝑧)}) |
5 | df-co 5642 | . 2 ⊢ (𝐶 ∘ 𝐴) = {〈𝑥, 𝑧〉 ∣ ∃𝑦(𝑥𝐴𝑦 ∧ 𝑦𝐶𝑧)} | |
6 | df-co 5642 | . 2 ⊢ (𝐶 ∘ 𝐵) = {〈𝑥, 𝑧〉 ∣ ∃𝑦(𝑥𝐵𝑦 ∧ 𝑦𝐶𝑧)} | |
7 | 4, 5, 6 | 3sstr4g 3989 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∃wex 1781 ⊆ wss 3910 class class class wbr 5105 {copab 5167 ∘ ccom 5637 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-v 3447 df-in 3917 df-ss 3927 df-br 5106 df-opab 5168 df-co 5642 |
This theorem is referenced by: coeq2 5814 funss 6520 tposss 8157 dftpos4 8175 ttrclco 9653 frmin 9684 frrlem16 9693 rtrclreclem4 14945 tsrdir 18492 mvdco 19225 ustex2sym 23566 ustex3sym 23567 ustneism 23573 trust 23579 utop2nei 23600 neipcfilu 23646 fcoinver 31472 trclubgNEW 41871 trrelsuperrel2dg 41924 |
Copyright terms: Public domain | W3C validator |