![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ss2ixp | Structured version Visualization version GIF version |
Description: Subclass theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.) (Revised by Mario Carneiro, 12-Aug-2016.) |
Ref | Expression |
---|---|
ss2ixp | ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → X𝑥 ∈ 𝐴 𝐵 ⊆ X𝑥 ∈ 𝐴 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssel 3989 | . . . . 5 ⊢ (𝐵 ⊆ 𝐶 → ((𝑓‘𝑥) ∈ 𝐵 → (𝑓‘𝑥) ∈ 𝐶)) | |
2 | 1 | ral2imi 3083 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵 → ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶)) |
3 | 2 | anim2d 612 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ((𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵) → (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶))) |
4 | 3 | ss2abdv 4076 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → {𝑓 ∣ (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)} ⊆ {𝑓 ∣ (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶)}) |
5 | df-ixp 8937 | . 2 ⊢ X𝑥 ∈ 𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)} | |
6 | df-ixp 8937 | . 2 ⊢ X𝑥 ∈ 𝐴 𝐶 = {𝑓 ∣ (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶)} | |
7 | 4, 5, 6 | 3sstr4g 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 |