Theorem coexg 7905

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 6245	. 2 ⊢ (𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴)
2		dmexg 7877	. . 3 ⊢ (𝐵 ∈ 𝑊 → dom 𝐵 ∈ V)
3		rnexg 7878	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
4		xpexg 7726	. . 3 ⊢ ((dom 𝐵 ∈ V ∧ ran 𝐴 ∈ V) → (dom 𝐵 × ran 𝐴) ∈ V)
5	2, 3, 4	syl2anr 597	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (dom 𝐵 × ran 𝐴) ∈ V)
6		ssexg 5278	. 2 ⊢ (((𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴) ∧ (dom 𝐵 × ran 𝐴) ∈ V) → (𝐴 ∘ 𝐵) ∈ V)
7	1, 5, 6	sylancr 587	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∘ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Vcvv 3447   ⊆ wss 3914   × cxp 5636  dom cdm 5638  ran crn 5639   ∘ ccom 5642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649

This theorem is referenced by:  coex  7906  coexd  7907  suppco  8185  fsuppco2  9354  fsuppcor  9355  mapfienlem2  9357  wemapwe  9650  cofsmo  10222  relexpsucnnr  14991  supcvg  15822  imasle  17486  setcco  18045  estrcco  18091  pwsco1mhm  18759  pwsco2mhm  18760  efmndov  18808  efmndcl  18809  symgov  19314  symgcl  19315  gsumval3lem2  19836  gsumzf1o  19842  f1lindf  21731  evls1sca  22210  tngds  24536  climcncf  24793  motplusg  28469  tocycfv  33066  smatfval  33785  eulerpartlemmf  34366  hgt750lemg  34645  cossex  38410  tgrpov  40742  erngmul  40800  erngmul-rN  40808  dvamulr  41006  dvavadd  41009  dvhmulr  41080  mendmulr  43173  relexp0a  43705  choicefi  45194  climexp  45603  dvsinax  45911  stoweidlem27  46025  stoweidlem31  46029  stoweidlem59  46057  grimco  47889  uspgrbisymrelALT  48143  rngccoALTV  48259  ringccoALTV  48293  itcoval1  48652  itcoval2  48653  itcoval3  48654  itcovalsucov  48657