Theorem ssxp 3345

Description: Subset theorem for cross product. Generalization of Theorem 101 of [Suppes] p. 52.

Assertion

Ref	Expression
ssxp	|- ((A (_ B /\ C (_ D) -> (A X. C) (_ (B X. D))

Proof of Theorem ssxp

Step	Hyp	Ref	Expression
1		relxp 3344	. . 3 |- Rel (A X. C)
2	1	a1i 8	. 2 |- ((A (_ B /\ C (_ D) -> Rel (A X. C))
3		prth 559	. . . 4 |- (((x e. A -> x e. B) /\ (y e. C -> y e. D)) -> ((x e. A /\ y e. C) -> (x e. B /\ y e. D)))
4		visset 1859	. . . . 5 |- y e. V
5	4	opelxp 3297	. . . 4 |- (<.x, y>. e. (A X. C) <-> (x e. A /\ y e. C))
6	4	opelxp 3297	. . . 4 |- (<.x, y>. e. (B X. D) <-> (x e. B /\ y e. D))
7	3, 5, 6	3imtr4g 556	. . 3 |- (((x e. A -> x e. B) /\ (y e. C -> y e. D)) -> (<.x, y>. e. (A X. C) -> <.x, y>. e. (B X. D)))
8		ssel 2115	. . 3 |- (A (_ B -> (x e. A -> x e. B))
9		ssel 2115	. . 3 |- (C (_ D -> (y e. C -> y e. D))
10	7, 8, 9	syl2an 456	. 2 |- ((A (_ B /\ C (_ D) -> (<.x, y>. e. (A X. C) -> <.x, y>. e. (B X. D)))
11	2, 10	relssdv 3337	1 |- ((A (_ B /\ C (_ D) -> (A X. C) (_ (B X. D))

Syntax hints:   -> wi 3   /\ wa 221   e. wcel 994   (_ wss 2099  <.cop 2469   X. cxp 3249  Rel wrel 3256

This theorem is referenced by:  ssres2 3476  ssxpb 3560  ssrnres 3566  relrelss 3618  coexg 3629  fssxp 3744  funssxp 3745  oprabss 4066  xpdom3 4586  dmaddpi 5172  dmmulpi 5173  axresscn 5422  mulnzcnopr 5854  climuz0i 7311  xpnnen 7711  infxpidmlem7 7770  metreslem 8032  cncfmet 8116  remetba 8120  lmbrf 8141  iscauf 8150  iscau5 8152  iscaunns 8155  lmsslem 8163  caussi 8165  lmclimnn 8175  resgrprn 8336  issubgi 8364  ghgrpilem4 8377  sspg 8641  ssps 8643  sspmlem 8645  h2hcau 9124  h2hlm 9125  hhssabli 9408  hhssnv 9410  hhshsslem1 9413  ghomfo 10676  residcp 10806  difxp 11798  stioo 11910  iccst 11939  txuni 11975  txsubsp 11983  txcld 11985  heiborlem33 12043  icccmp 12083  phtpycolem3 12095  phtpycolem4 12096

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777  ax-pow 2818  ax-pr 2855

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-v 1858  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-pw 2459  df-sn 2470  df-pr 2471  df-op 2474  df-opab 2741  df-xp 3265  df-rel 3266

Copyright terms: Public domain