MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ss2ixp Structured version   Visualization version   GIF version

Theorem ss2ixp 8903
Description: Subclass theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.) (Revised by Mario Carneiro, 12-Aug-2016.)
Assertion
Ref Expression
ss2ixp (∀𝑥𝐴 𝐵𝐶X𝑥𝐴 𝐵X𝑥𝐴 𝐶)

Proof of Theorem ss2ixp
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 ssel 3975 . . . . 5 (𝐵𝐶 → ((𝑓𝑥) ∈ 𝐵 → (𝑓𝑥) ∈ 𝐶))
21ral2imi 3085 . . . 4 (∀𝑥𝐴 𝐵𝐶 → (∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵 → ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐶))
32anim2d 612 . . 3 (∀𝑥𝐴 𝐵𝐶 → ((𝑓 Fn {𝑥𝑥𝐴} ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵) → (𝑓 Fn {𝑥𝑥𝐴} ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐶)))
43ss2abdv 4060 . 2 (∀𝑥𝐴 𝐵𝐶 → {𝑓 ∣ (𝑓 Fn {𝑥𝑥𝐴} ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵)} ⊆ {𝑓 ∣ (𝑓 Fn {𝑥𝑥𝐴} ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐶)})
5 df-ixp 8891 . 2 X𝑥𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn {𝑥𝑥𝐴} ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵)}
6 df-ixp 8891 . 2 X𝑥𝐴 𝐶 = {𝑓 ∣ (𝑓 Fn {𝑥𝑥𝐴} ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐶)}
74, 5, 63sstr4g 4027 1 (∀𝑥𝐴 𝐵𝐶X𝑥𝐴 𝐵X𝑥𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2106  {cab 2709  wral 3061  wss 3948   Fn wfn 6538  cfv 6543  Xcixp 8890
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-v 3476  df-in 3955  df-ss 3965  df-ixp 8891
This theorem is referenced by:  ixpeq2  8904  boxcutc  8934  pwcfsdom  10577  prdsvallem  17399  prdshom  17412  sscpwex  17761  wunfunc  17848  wunfuncOLD  17849  wunnat  17906  wunnatOLD  17907  dprdss  19898  psrbaglefi  21484  psrbaglefiOLD  21485  ptuni2  23079  ptcld  23116  ptclsg  23118  prdstopn  23131  xkopt  23158  tmdgsum2  23599  ressprdsds  23876  prdsbl  23999  ptrecube  36483  prdstotbnd  36657  ixpssixp  43771  ioorrnopnxrlem  45012  ovnlecvr2  45316
  Copyright terms: Public domain W3C validator