Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > dmcoss | Structured version Visualization version GIF version |
Description: Domain of a composition. Theorem 21 of [Suppes] p. 63. (Contributed by NM, 19-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Ref | Expression |
---|---|
dmcoss | ⊢ dom (𝐴 ∘ 𝐵) ⊆ dom 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfe1 2153 | . . . 4 ⊢ Ⅎ𝑦∃𝑦 𝑥𝐵𝑦 | |
2 | exsimpl 1876 | . . . . 5 ⊢ (∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) → ∃𝑧 𝑥𝐵𝑧) | |
3 | vex 3426 | . . . . . 6 ⊢ 𝑥 ∈ V | |
4 | vex 3426 | . . . . . 6 ⊢ 𝑦 ∈ V | |
5 | 3, 4 | opelco 5757 | . . . . 5 ⊢ (〈𝑥, 𝑦〉 ∈ (𝐴 ∘ 𝐵) ↔ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)) |
6 | breq2 5073 | . . . . . 6 ⊢ (𝑦 = 𝑧 → (𝑥𝐵𝑦 ↔ 𝑥𝐵𝑧)) | |
7 | 6 | cbvexvw 2045 | . . . . 5 ⊢ (∃𝑦 𝑥𝐵𝑦 ↔ ∃𝑧 𝑥𝐵𝑧) |
8 | 2, 5, 7 | 3imtr4i 295 | . . . 4 ⊢ (〈𝑥, 𝑦〉 ∈ (𝐴 ∘ 𝐵) → ∃𝑦 𝑥𝐵𝑦) |
9 | 1, 8 | exlimi 2217 | . . 3 ⊢ (∃𝑦〈𝑥, 𝑦〉 ∈ (𝐴 ∘ 𝐵) → ∃𝑦 𝑥𝐵𝑦) |
10 | 3 | eldm2 5787 | . . 3 ⊢ (𝑥 ∈ dom (𝐴 ∘ 𝐵) ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ (𝐴 ∘ 𝐵)) |
11 | 3 | eldm 5786 | . . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦 𝑥𝐵𝑦) |
12 | 9, 10, 11 | 3imtr4i 295 | . 2 ⊢ (𝑥 ∈ dom (𝐴 ∘ 𝐵) → 𝑥 ∈ dom 𝐵) |
13 | 12 | ssriv 3921 | 1 ⊢ dom (𝐴 ∘ 𝐵) ⊆ dom 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 399 ∃wex 1787 ∈ wcel 2112 ⊆ wss 3882 〈cop 4563 class class class wbr 5069 dom cdm 5568 ∘ ccom 5572 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-12 2177 ax-ext 2710 ax-sep 5208 ax-nul 5215 ax-pr 5338 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-clab 2717 df-cleq 2731 df-clel 2818 df-rab 3072 df-v 3424 df-dif 3885 df-un 3887 df-in 3889 df-ss 3899 df-nul 4254 df-if 4456 df-sn 4558 df-pr 4560 df-op 4564 df-br 5070 df-opab 5132 df-co 5577 df-dm 5578 |
This theorem is referenced by: rncoss 5858 dmcosseq 5859 cossxp 6152 fvco4i 6833 cofunexg 7743 fin23lem30 9983 wunco 10374 relexpnndm 14634 mvdco 18867 f1omvdconj 18868 znleval 20549 ofco2 21377 tngtopn 23577 xppreima 30731 cycpmrn 31158 relexp0a 41036 dmtrclfvRP 41050 |
Copyright terms: Public domain | W3C validator |