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

Theorem ss2ixp 8162
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 3793 . . . . 5 (𝐵𝐶 → ((𝑓𝑥) ∈ 𝐵 → (𝑓𝑥) ∈ 𝐶))
21ral2imi 3129 . . . 4 (∀𝑥𝐴 𝐵𝐶 → (∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵 → ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐶))
32anim2d 606 . . 3 (∀𝑥𝐴 𝐵𝐶 → ((𝑓 Fn {𝑥𝑥𝐴} ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵) → (𝑓 Fn {𝑥𝑥𝐴} ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐶)))
43ss2abdv 3872 . 2 (∀𝑥𝐴 𝐵𝐶 → {𝑓 ∣ (𝑓 Fn {𝑥𝑥𝐴} ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵)} ⊆ {𝑓 ∣ (𝑓 Fn {𝑥𝑥𝐴} ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐶)})
5 df-ixp 8150 . 2 X𝑥𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn {𝑥𝑥𝐴} ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵)}
6 df-ixp 8150 . 2 X𝑥𝐴 𝐶 = {𝑓 ∣ (𝑓 Fn {𝑥𝑥𝐴} ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐶)}
74, 5, 63sstr4g 3843 1 (∀𝑥𝐴 𝐵𝐶X𝑥𝐴 𝐵X𝑥𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385  wcel 2157  {cab 2786  wral 3090  wss 3770   Fn wfn 6097  cfv 6102  Xcixp 8149
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2378  ax-ext 2778
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2787  df-cleq 2793  df-clel 2796  df-nfc 2931  df-ral 3095  df-in 3777  df-ss 3784  df-ixp 8150
This theorem is referenced by:  ixpeq2  8163  boxcutc  8192  pwcfsdom  9694  prdsval  16429  prdshom  16441  sscpwex  16788  wunfunc  16872  wunnat  16929  dprdss  18743  psrbaglefi  19694  ptuni2  21707  ptcld  21744  ptclsg  21746  prdstopn  21759  xkopt  21786  tmdgsum2  22227  ressprdsds  22503  prdsbl  22623  ptrecube  33897  prdstotbnd  34079  ixpssixp  40023  ioorrnopnxrlem  41264  ovnlecvr2  41565
  Copyright terms: Public domain W3C validator