![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > coexg | Structured version Visualization version GIF version |
Description: The composition of two sets is a set. (Contributed by NM, 19-Mar-1998.) |
Ref | Expression |
---|---|
coexg | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∘ 𝐵) ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cossxp 6303 | . 2 ⊢ (𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴) | |
2 | dmexg 7941 | . . 3 ⊢ (𝐵 ∈ 𝑊 → dom 𝐵 ∈ V) | |
3 | rnexg 7942 | . . 3 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V) | |
4 | xpexg 7785 | . . 3 ⊢ ((dom 𝐵 ∈ V ∧ ran 𝐴 ∈ V) → (dom 𝐵 × ran 𝐴) ∈ V) | |
5 | 2, 3, 4 | syl2anr 596 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (dom 𝐵 × ran 𝐴) ∈ V) |
6 | ssexg 5341 | . 2 ⊢ (((𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴) ∧ (dom 𝐵 × ran 𝐴) ∈ V) → (𝐴 ∘ 𝐵) ∈ V) | |
7 | 1, 5, 6 | sylancr 586 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∘ 𝐵) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2108 Vcvv 3488 ⊆ wss 3976 × cxp 5698 dom cdm 5700 ran crn 5701 ∘ ccom 5704 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-12 2178 ax-ext 2711 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-clab 2718 df-cleq 2732 df-clel 2819 df-ral 3068 df-rex 3077 df-rab 3444 df-v 3490 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-br 5167 df-opab 5229 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 |
This theorem is referenced by: coex 7970 coexd 7971 suppco 8247 fsuppco2 9472 fsuppcor 9473 mapfienlem2 9475 wemapwe 9766 cofsmo 10338 relexpsucnnr 15074 supcvg 15904 imasle 17583 setcco 18150 estrcco 18198 pwsco1mhm 18867 pwsco2mhm 18868 efmndov 18916 efmndcl 18917 symgov 19425 symgcl 19426 gsumval3lem2 19948 gsumzf1o 19954 f1lindf 21865 evls1sca 22348 tngds 24689 tngdsOLD 24690 climcncf 24945 motplusg 28568 tocycfv 33102 smatfval 33741 eulerpartlemmf 34340 hgt750lemg 34631 cossex 38375 tgrpov 40705 erngmul 40763 erngmul-rN 40771 dvamulr 40969 dvavadd 40972 dvhmulr 41043 mendmulr 43145 relexp0a 43678 choicefi 45107 climexp 45526 dvsinax 45834 stoweidlem27 45948 stoweidlem31 45952 stoweidlem59 45980 grimco 47764 uspgrbisymrelALT 47878 rngccoALTV 47994 ringccoALTV 48028 itcoval1 48397 itcoval2 48398 itcoval3 48399 itcovalsucov 48402 |
Copyright terms: Public domain | W3C validator |