Theorem coexg 7939

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 6273	. 2 ⊢ (𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴)
2		dmexg 7911	. . 3 ⊢ (𝐵 ∈ 𝑊 → dom 𝐵 ∈ V)
3		rnexg 7912	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
4		xpexg 7762	. . 3 ⊢ ((dom 𝐵 ∈ V ∧ ran 𝐴 ∈ V) → (dom 𝐵 × ran 𝐴) ∈ V)
5	2, 3, 4	syl2anr 609	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (dom 𝐵 × ran 𝐴) ∈ V)
6		ssexg 5281	. 2 ⊢ (((𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴) ∧ (dom 𝐵 × ran 𝐴) ∈ V) → (𝐴 ∘ 𝐵) ∈ V)
7	1, 5, 6	sylancr 599	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∘ 𝐵) ∈ V)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  Vcvv 3451   ⊆ wss 3899   × cxp 5649  dom cdm 5651  ran crn 5652   ∘ ccom 5655

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pow 5327  ax-pr 5391  ax-un 7749

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662

This theorem is used by:  coex  7940  coexd  7941  suppco  8216  fsuppco2  9388  fsuppcor  9389  mapfienlem2  9391  wemapwe  9691  cofsmo  10340  relexpsucnnr  15171  supcvg  16018  imasle  17688  setcco  18251  estrcco  18297  pwsco1mhm  19021  pwsco2mhm  19022  efmndov  19070  efmndcl  19071  symgov  19591  symgcl  19592  gsumval3lem2  20113  gsumzf1o  20119  f1lindf  22121  evls1sca  22634  tngds  24960  climcncf  25214  motplusg  28998  tocycfv  33663  smatfval  34420  eulerpartlemmf  35000  hgt750lemg  35276  cossex  39421  tgrpov  41785  erngmul  41843  erngmul-rN  41851  dvamulr  42049  dvavadd  42052  dvhmulr  42123  mendmulr  44170  relexp0a  44701  choicefi  46183  climexp  46586  dvsinax  46892  stoweidlem27  47006  stoweidlem31  47010  stoweidlem59  47038  grimco  48956  uspgrbisymrelALT  49222  rngccoALTV  49337  ringccoALTV  49371  itcoval1  49744  itcoval2  49745  itcoval3  49746  itcovalsucov  49749