Theorem ssxp 3246

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 3245	. . 3 |- Rel (A X. C)
2	1	a1i 8	. 2 |- ((A (_ B /\ C (_ D) -> Rel (A X. C))
3		prth 554	. . . 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 1804	. . . . 5 |- y e. V
5	4	opelxp 3204	. . . 4 |- (<.x, y>. e. (A X. C) <-> (x e. A /\ y e. C))
6	4	opelxp 3204	. . . 4 |- (<.x, y>. e. (B X. D) <-> (x e. B /\ y e. D))
7	3, 5, 6	3imtr4g 551	. . 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 2053	. . 3 |- (A (_ B -> (x e. A -> x e. B))
9		ssel 2053	. . 3 |- (C (_ D -> (y e. C -> y e. D))
10	7, 8, 9	syl2an 454	. 2 |- ((A (_ B /\ C (_ D) -> (<.x, y>. e. (A X. C) -> <.x, y>. e. (B X. D)))
11	2, 10	relssdv 3239	1 |- ((A (_ B /\ C (_ D) -> (A X. C) (_ (B X. D))

Syntax hints:   -> wi 3   /\ wa 223   e. wcel 955   (_ wss 2037  <.cop 2401   X. cxp 3158  Rel wrel 3165

This theorem is referenced by:  ssres2 3370  ssrnres 3467  coexg 3510  fssxp 3622  funssxp 3623  oprabss 3991  xpdom3 4425  dmaddpi 4990  dmmulpi 4991  axresscn 5240  mulnzcnopr 5671  climuz0 7045  xpnnen 7441  infxpidmlem7 7501  metreslem 7762  cncfmet 7844  remetba 7848  lmbrf 7868  iscauf 7877  iscau5 7878  lmsslem 7887  caussi 7889  lmclimnn 7899  resgrprn 8030  resgrprnOLD 8031  issubgi 8059  ghgrpilem4 8073  sspg 8321  ssps 8323  sspmlem 8325  circgrpOLD 8658  h2hcau 8788  h2hlm 8789  hhssabl 9053  hhssnv 9054  hhshsslem1 9057  ghomfo 10296

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-pow 2732  ax-pr 2769

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406  df-opab 2657  df-xp 3174  df-rel 3175

Copyright terms: Public domain