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 3868 | . . . . 5 ⊢ (𝐵 ⊆ 𝐶 → ((𝑓‘𝑥) ∈ 𝐵 → (𝑓‘𝑥) ∈ 𝐶)) | |
2 | 1 | ral2imi 3071 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵 → ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶)) |
3 | 2 | anim2d 615 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ((𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵) → (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶))) |
4 | 3 | ss2abdv 3951 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → {𝑓 ∣ (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)} ⊆ {𝑓 ∣ (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶)}) |
5 | df-ixp 8501 | . 2 ⊢ X𝑥 ∈ 𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)} | |
6 | df-ixp 8501 | . 2 ⊢ X𝑥 ∈ 𝐴 𝐶 = {𝑓 ∣ (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶)} | |
7 | 4, 5, 6 | 3sstr4g 3920 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → X𝑥 ∈ 𝐴 𝐵 ⊆ X𝑥 ∈ 𝐴 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∈ wcel 2113 {cab 2716 ∀wral 3053 ⊆ wss 3841 Fn wfn 6328 ‘cfv 6333 Xcixp 8500 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1545 df-ex 1787 df-sb 2074 df-clab 2717 df-cleq 2730 df-clel 2811 df-ral 3058 df-v 3399 df-in 3848 df-ss 3858 df-ixp 8501 |
This theorem is referenced by: ixpeq2 8514 boxcutc 8544 pwcfsdom 10076 prdsval 16824 prdshom 16836 sscpwex 17183 wunfunc 17267 wunnat 17324 dprdss 19263 psrbaglefi 20738 psrbaglefiOLD 20739 ptuni2 22320 ptcld 22357 ptclsg 22359 prdstopn 22372 xkopt 22399 tmdgsum2 22840 ressprdsds 23117 prdsbl 23237 ptrecube 35389 prdstotbnd 35564 ixpssixp 42164 ioorrnopnxrlem 43373 ovnlecvr2 43674 |
Copyright terms: Public domain | W3C validator |