Theorem coexg 7447

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 5959	. 2 ⊢ (𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴)
2		dmexg 7426	. . 3 ⊢ (𝐵 ∈ 𝑊 → dom 𝐵 ∈ V)
3		rnexg 7427	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
4		xpexg 7288	. . 3 ⊢ ((dom 𝐵 ∈ V ∧ ran 𝐴 ∈ V) → (dom 𝐵 × ran 𝐴) ∈ V)
5	2, 3, 4	syl2anr 587	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (dom 𝐵 × ran 𝐴) ∈ V)
6		ssexg 5081	. 2 ⊢ (((𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴) ∧ (dom 𝐵 × ran 𝐴) ∈ V) → (𝐴 ∘ 𝐵) ∈ V)
7	1, 5, 6	sylancr 578	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∘ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 387   ∈ wcel 2048  Vcvv 3412   ⊆ wss 3828   × cxp 5402  dom cdm 5404  ran crn 5405   ∘ ccom 5408

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2747  ax-sep 5058  ax-nul 5065  ax-pow 5117  ax-pr 5184  ax-un 7277

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-ral 3090  df-rex 3091  df-rab 3094  df-v 3414  df-dif 3831  df-un 3833  df-in 3835  df-ss 3842  df-nul 4178  df-if 4349  df-pw 4422  df-sn 4440  df-pr 4442  df-op 4446  df-uni 4711  df-br 4928  df-opab 4990  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415

This theorem is referenced by:  coex  7448  suppco  7670  supp0cosupp0OLD  7673  imacosuppOLD  7675  fsuppco2  8657  fsuppcor  8658  mapfienlem2  8660  wemapwe  8950  cofsmo  9485  relexpsucnnr  14239  supcvg  15065  imasle  16646  setcco  17195  estrcco  17232  pwsco1mhm  17832  pwsco2mhm  17833  symgov  18273  symgcl  18274  gsumval3lem2  18774  gsumzf1o  18780  evls1sca  20183  f1lindf  20662  tngds  22954  climcncf  23205  motplusg  26024  smatfval  30693  eulerpartlemmf  31269  hgt750lemg  31564  cossex  35087  tgrpov  37307  erngmul  37365  erngmul-rN  37373  dvamulr  37571  dvavadd  37574  dvhmulr  37645  mendmulr  39162  relexp0a  39402  choicefi  40867  climexp  41296  dvsinax  41606  stoweidlem27  41722  stoweidlem31  41726  stoweidlem59  41754  uspgrbisymrelALT  43372  rngccoALTV  43597  ringccoALTV  43660