![]() |
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 3938 | . . . . 5 ⊢ (𝐵 ⊆ 𝐶 → ((𝑓‘𝑥) ∈ 𝐵 → (𝑓‘𝑥) ∈ 𝐶)) | |
2 | 1 | ral2imi 3085 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵 → ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶)) |
3 | 2 | anim2d 613 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ((𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵) → (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶))) |
4 | 3 | ss2abdv 4021 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → {𝑓 ∣ (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)} ⊆ {𝑓 ∣ (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶)}) |
5 | df-ixp 8839 | . 2 ⊢ X𝑥 ∈ 𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)} | |
6 | df-ixp 8839 | . 2 ⊢ X𝑥 ∈ 𝐴 𝐶 = {𝑓 ∣ (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶)} | |
7 | 4, 5, 6 | 3sstr4g 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 |