![]() |
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 2194 | . . . 4 ⊢ Ⅎ𝑦∃𝑦 𝑥𝐵𝑦 | |
2 | exsimpl 1966 | . . . . 5 ⊢ (∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) → ∃𝑧 𝑥𝐵𝑧) | |
3 | vex 3388 | . . . . . 6 ⊢ 𝑥 ∈ V | |
4 | vex 3388 | . . . . . 6 ⊢ 𝑦 ∈ V | |
5 | 3, 4 | opelco 5497 | . . . . 5 ⊢ (〈𝑥, 𝑦〉 ∈ (𝐴 ∘ 𝐵) ↔ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)) |
6 | breq2 4847 | . . . . . 6 ⊢ (𝑦 = 𝑧 → (𝑥𝐵𝑦 ↔ 𝑥𝐵𝑧)) | |
7 | 6 | cbvexvw 2139 | . . . . 5 ⊢ (∃𝑦 𝑥𝐵𝑦 ↔ ∃𝑧 𝑥𝐵𝑧) |
8 | 2, 5, 7 | 3imtr4i 284 | . . . 4 ⊢ (〈𝑥, 𝑦〉 ∈ (𝐴 ∘ 𝐵) → ∃𝑦 𝑥𝐵𝑦) |
9 | 1, 8 | exlimi 2252 | . . 3 ⊢ (∃𝑦〈𝑥, 𝑦〉 ∈ (𝐴 ∘ 𝐵) → ∃𝑦 𝑥𝐵𝑦) |
10 | 3 | eldm2 5525 | . . 3 ⊢ (𝑥 ∈ dom (𝐴 ∘ 𝐵) ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ (𝐴 ∘ 𝐵)) |
11 | 3 | eldm 5524 | . . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦 𝑥𝐵𝑦) |
12 | 9, 10, 11 | 3imtr4i 284 | . 2 ⊢ (𝑥 ∈ dom (𝐴 ∘ 𝐵) → 𝑥 ∈ dom 𝐵) |
13 | 12 | ssriv 3802 | 1 ⊢ dom (𝐴 ∘ 𝐵) ⊆ dom 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 385 ∃wex 1875 ∈ wcel 2157 ⊆ wss 3769 〈cop 4374 class class class wbr 4843 dom cdm 5312 ∘ ccom 5316 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2777 ax-sep 4975 ax-nul 4983 ax-pr 5097 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2591 df-eu 2609 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-rab 3098 df-v 3387 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-nul 4116 df-if 4278 df-sn 4369 df-pr 4371 df-op 4375 df-br 4844 df-opab 4906 df-co 5321 df-dm 5322 |
This theorem is referenced by: rncoss 5590 dmcosseq 5591 cossxp 5877 fvco4i 6501 cofunexg 7365 fin23lem30 9452 wunco 9843 relexpnndm 14122 mvdco 18177 f1omvdconj 18178 znleval 20224 ofco2 20583 tngtopn 22782 xppreima 29968 relexp0a 38791 dmtrclfvRP 38805 |
Copyright terms: Public domain | W3C validator |