| 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 3977 | . . . . 5 ⊢ (𝐵 ⊆ 𝐶 → ((𝑓‘𝑥) ∈ 𝐵 → (𝑓‘𝑥) ∈ 𝐶)) | |
| 2 | 1 | ral2imi 3085 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵 → ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶)) |
| 3 | 2 | anim2d 612 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ((𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵) → (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶))) |
| 4 | 3 | ss2abdv 4066 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → {𝑓 ∣ (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)} ⊆ {𝑓 ∣ (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶)}) |
| 5 | df-ixp 8938 | . 2 ⊢ X𝑥 ∈ 𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)} | |
| 6 | df-ixp 8938 | . 2 ⊢ X𝑥 ∈ 𝐴 𝐶 = {𝑓 ∣ (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶)} | |
| 7 | 4, 5, 6 | 3sstr4g 4037 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → X𝑥 ∈ 𝐴 𝐵 ⊆ X𝑥 ∈ 𝐴 𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2108 {cab 2714 ∀wral 3061 ⊆ wss 3951 Fn wfn 6556 ‘cfv 6561 Xcixp 8937 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-ss 3968 df-ixp 8938 |
| This theorem is referenced by: ixpeq2 8951 boxcutc 8981 pwcfsdom 10623 prdsvallem 17499 prdshom 17512 sscpwex 17859 wunfunc 17946 wunnat 18004 dprdss 20049 psrbaglefi 21946 ptuni2 23584 ptcld 23621 ptclsg 23623 prdstopn 23636 xkopt 23663 tmdgsum2 24104 ressprdsds 24381 prdsbl 24504 ptrecube 37627 prdstotbnd 37801 ixpssixp 45097 ioorrnopnxrlem 46321 ovnlecvr2 46625 |
| Copyright terms: Public domain | W3C validator |