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

Theorem ss2ixp 8949
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 3989 . . . . 5 (𝐵𝐶 → ((𝑓𝑥) ∈ 𝐵 → (𝑓𝑥) ∈ 𝐶))
21ral2imi 3083 . . . 4 (∀𝑥𝐴 𝐵𝐶 → (∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵 → ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐶))
32anim2d 612 . . 3 (∀𝑥𝐴 𝐵𝐶 → ((𝑓 Fn {𝑥𝑥𝐴} ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵) → (𝑓 Fn {𝑥𝑥𝐴} ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐶)))
43ss2abdv 4076 . 2 (∀𝑥𝐴 𝐵𝐶 → {𝑓 ∣ (𝑓 Fn {𝑥𝑥𝐴} ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵)} ⊆ {𝑓 ∣ (𝑓 Fn {𝑥𝑥𝐴} ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐶)})
5 df-ixp 8937 . 2 X𝑥𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn {𝑥𝑥𝐴} ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵)}
6 df-ixp 8937 . 2 X𝑥𝐴 𝐶 = {𝑓 ∣ (𝑓 Fn {𝑥𝑥𝐴} ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐶)}
74, 5, 63sstr4g 4041 1 (∀𝑥𝐴 𝐵𝐶X𝑥𝐴 𝐵X𝑥𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wcel 2106  {cab 2712  wral 3059  wss 3963   Fn wfn 6558  cfv 6563  Xcixp 8936
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-ss 3980  df-ixp 8937
This theorem is referenced by:  ixpeq2  8950  boxcutc  8980  pwcfsdom  10621  prdsvallem  17501  prdshom  17514  sscpwex  17863  wunfunc  17952  wunfuncOLD  17953  wunnat  18011  wunnatOLD  18012  dprdss  20064  psrbaglefi  21964  ptuni2  23600  ptcld  23637  ptclsg  23639  prdstopn  23652  xkopt  23679  tmdgsum2  24120  ressprdsds  24397  prdsbl  24520  ptrecube  37607  prdstotbnd  37781  ixpssixp  45032  ioorrnopnxrlem  46262  ovnlecvr2  46566
  Copyright terms: Public domain W3C validator