Theorem coexg 7926

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 6269	. 2 ⊢ (𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴)
2		dmexg 7898	. . 3 ⊢ (𝐵 ∈ 𝑊 → dom 𝐵 ∈ V)
3		rnexg 7899	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
4		xpexg 7749	. . 3 ⊢ ((dom 𝐵 ∈ V ∧ ran 𝐴 ∈ V) → (dom 𝐵 × ran 𝐴) ∈ V)
5	2, 3, 4	syl2anr 609	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (dom 𝐵 × ran 𝐴) ∈ V)
6		ssexg 5284	. 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 3450   ⊆ wss 3899   × cxp 5653  dom cdm 5655  ran crn 5656   ∘ ccom 5659

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 2732  ax-sep 5251  ax-pow 5330  ax-pr 5398  ax-un 7736

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 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666

This theorem is used by:  coex  7927  coexd  7928  suppco  8204  fsuppco2  9373  fsuppcor  9374  mapfienlem2  9376  wemapwe  9676  cofsmo  10271  relexpsucnnr  15098  supcvg  15945  imasle  17609  setcco  18172  estrcco  18218  pwsco1mhm  18941  pwsco2mhm  18942  efmndov  18990  efmndcl  18991  symgov  19511  symgcl  19512  gsumval3lem2  20033  gsumzf1o  20039  f1lindf  22035  evls1sca  22548  tngds  24874  climcncf  25128  motplusg  28884  tocycfv  33549  smatfval  34305  eulerpartlemmf  34886  hgt750lemg  35162  cossex  39257  tgrpov  41621  erngmul  41679  erngmul-rN  41687  dvamulr  41885  dvavadd  41888  dvhmulr  41959  mendmulr  44025  relexp0a  44556  choicefi  46031  climexp  46435  dvsinax  46741  stoweidlem27  46855  stoweidlem31  46859  stoweidlem59  46887  grimco  48805  uspgrbisymrelALT  49071  rngccoALTV  49186  ringccoALTV  49220  itcoval1  49593  itcoval2  49594  itcoval3  49595  itcovalsucov  49598