Theorem xpex 3255

Description: The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23.

Hypotheses

Ref	Expression
xpex.1	|- A e. V
xpex.2	|- B e. V

Assertion

Ref	Expression
xpex	|- (A X. B) e. V

Proof of Theorem xpex

Step	Hyp	Ref	Expression
1		xpex.1	. 2 |- A e. V
2		xpex.2	. 2 |- B e. V
3		xpexg 3254	. 2 |- ((A e. V /\ B e. V) -> (A X. B) e. V)
4	1, 2, 3	mp2an 696	1 |- (A X. B) e. V

Syntax hints:   e. wcel 956  Vcvv 1807   X. cxp 3163

This theorem is referenced by:  oprabex 4010  oprabex3 4013  oprvalex 4032  elpm 4326  map0 4334  map1 4417  xpsnen 4421  endisj 4423  xpcomen 4425  xpassen 4427  xpdom2 4428  xpdom3 4431  xpen 4474  mapxpen 4481  xpmapenlem5 4486  rankxpl 4690  rankxplim 4692  rankxplim2 4693  rankxplim3 4694  rankxpsuc 4695  aceq3 4713  aceq5lem2 4716  aceq5lem3 4717  weth 4767  unxpdomlem 4823  unxpdom2 4825  sucxpdom 4826  uncdadom 4901  cdaassen 4910  xpcdaen 4911  mapcdaen 4912  cdadom1 4913  enqex 5028  nqex 5029  enrex 5158  srex 5159  axcnex 5247  addex 5297  mulex 5298  exp1t 6513  expp1t 6514  serz0 6999  serzcmp0 7001  climconst2 7040  climconst3 7041  climuz0 7053  climaddc1 7062  climmulc2 7073  climsubc2 7075  climcmpc1 7083  iserzcmp0 7087  ser1const 7115  acdc3lem 7436  acdclem 7444  xpnnen 7449  xpomen 7450  qnnen 7454  ruclem9 7469  infxpidmlem1 7503  infxpidmlem9 7511  infxpidmlem10 7512  infxpidmlem12 7514  infmap1 7524  iunctb 7525  infmap2lem2 7530  infmap2 7531  ismeti 7752  metxp 7786  lmclim 7914  metelcls 7916  bcthlem12 7960  bcthlem15 7963  bcthlem30 7978  isgrpi 7992  isgrp2i 8026  vcoprne 8150  sspval 8329  0ofval 8392  ajfval 8413  hvmulex 8820  hlim0 9044  hlimcau 9046  hlimuni 9048

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-pow 2737  ax-pr 2774  ax-un 2861

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-op 2412  df-uni 2499  df-opab 2662  df-xp 3179  df-rel 3180

Copyright terms: Public domain