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

Theorem ss2ixp 8851
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 3938 . . . . 5 (𝐵𝐶 → ((𝑓𝑥) ∈ 𝐵 → (𝑓𝑥) ∈ 𝐶))
21ral2imi 3085 . . . 4 (∀𝑥𝐴 𝐵𝐶 → (∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵 → ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐶))
32anim2d 613 . . 3 (∀𝑥𝐴 𝐵𝐶 → ((𝑓 Fn {𝑥𝑥𝐴} ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵) → (𝑓 Fn {𝑥𝑥𝐴} ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐶)))
43ss2abdv 4021 . 2 (∀𝑥𝐴 𝐵𝐶 → {𝑓 ∣ (𝑓 Fn {𝑥𝑥𝐴} ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵)} ⊆ {𝑓 ∣ (𝑓 Fn {𝑥𝑥𝐴} ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐶)})
5 df-ixp 8839 . 2 X𝑥𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn {𝑥𝑥𝐴} ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵)}
6 df-ixp 8839 . 2 X𝑥𝐴 𝐶 = {𝑓 ∣ (𝑓 Fn {𝑥𝑥𝐴} ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐶)}
74, 5, 63sstr4g 3990 1 (∀𝑥𝐴 𝐵𝐶X𝑥𝐴 𝐵X𝑥𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107  {cab 2710  wral 3061  wss 3911   Fn wfn 6492  cfv 6497  Xcixp 8838
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3062  df-v 3446  df-in 3918  df-ss 3928  df-ixp 8839
This theorem is referenced by:  ixpeq2  8852  boxcutc  8882  pwcfsdom  10524  prdsvallem  17341  prdshom  17354  sscpwex  17703  wunfunc  17790  wunfuncOLD  17791  wunnat  17848  wunnatOLD  17849  dprdss  19813  psrbaglefi  21350  psrbaglefiOLD  21351  ptuni2  22943  ptcld  22980  ptclsg  22982  prdstopn  22995  xkopt  23022  tmdgsum2  23463  ressprdsds  23740  prdsbl  23863  ptrecube  36124  prdstotbnd  36299  ixpssixp  43390  ioorrnopnxrlem  44633  ovnlecvr2  44937
  Copyright terms: Public domain W3C validator