Theorem coexg 7950

Description: The composition of two sets is a set. (Contributed by NM, 19-Mar-1998.)

Assertion

Ref	Expression
coexg	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∘ 𝐵) ∈ V)

Proof of Theorem coexg

Step	Hyp	Ref	Expression
1		cossxp 6288	. 2 ⊢ (𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴)
2		dmexg 7922	. . 3 ⊢ (𝐵 ∈ 𝑊 → dom 𝐵 ∈ V)
3		rnexg 7923	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
4		xpexg 7766	. . 3 ⊢ ((dom 𝐵 ∈ V ∧ ran 𝐴 ∈ V) → (dom 𝐵 × ran 𝐴) ∈ V)
5	2, 3, 4	syl2anr 595	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (dom 𝐵 × ran 𝐴) ∈ V)
6		ssexg 5331	. 2 ⊢ (((𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴) ∧ (dom 𝐵 × ran 𝐴) ∈ V) → (𝐴 ∘ 𝐵) ∈ V)
7	1, 5, 6	sylancr 585	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∘ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2100  Vcvv 3472   ⊆ wss 3959   × cxp 5684  dom cdm 5686  ran crn 5687   ∘ ccom 5690

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-12 2170  ax-ext 2700  ax-sep 5307  ax-nul 5314  ax-pow 5373  ax-pr 5437  ax-un 7751

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-clab 2707  df-cleq 2721  df-clel 2806  df-ral 3055  df-rex 3064  df-rab 3429  df-v 3474  df-dif 3962  df-un 3964  df-in 3966  df-ss 3976  df-nul 4336  df-if 4537  df-pw 4612  df-sn 4637  df-pr 4639  df-op 4643  df-uni 4919  df-br 5157  df-opab 5219  df-xp 5692  df-rel 5693  df-cnv 5694  df-co 5695  df-dm 5696  df-rn 5697

This theorem is referenced by:  coex  7951  coexd  7952  suppco  8229  fsuppco2  9453  fsuppcor  9454  mapfienlem2  9456  wemapwe  9747  cofsmo  10319  relexpsucnnr  15051  supcvg  15881  imasle  17559  setcco  18126  estrcco  18174  pwsco1mhm  18843  pwsco2mhm  18844  efmndov  18892  efmndcl  18893  symgov  19403  symgcl  19404  gsumval3lem2  19926  gsumzf1o  19932  f1lindf  21842  evls1sca  22337  tngds  24678  tngdsOLD  24679  climcncf  24934  motplusg  28492  tocycfv  33028  smatfval  33668  eulerpartlemmf  34267  hgt750lemg  34558  cossex  38184  tgrpov  40514  erngmul  40572  erngmul-rN  40580  dvamulr  40778  dvavadd  40781  dvhmulr  40852  mendmulr  42940  relexp0a  43474  choicefi  44897  climexp  45316  dvsinax  45624  stoweidlem27  45738  stoweidlem31  45742  stoweidlem59  45770  grimco  47549  uspgrbisymrelALT  47633  rngccoALTV  47749  ringccoALTV  47783  itcoval1  48152  itcoval2  48153  itcoval3  48154  itcovalsucov  48157