Metamath Proof Explorer

Theorem ss2ixp

Description: Subclass theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006) (Revised by Mario Carneiro, 12-Aug-2016)

Ref Expression
Assertion ss2ixp ⊢ ∀ x ∈ A B ⊆ C → ⨉ x ∈ A B ⊆ ⨉ x ∈ A C

Proof

Step Hyp Ref Expression
1 ssel ⊢ B ⊆ C → f ⁡ x ∈ B → f ⁡ x ∈ C
2 1 ral2imi ⊢ ∀ x ∈ A B ⊆ C → ∀ x ∈ A f ⁡ x ∈ B → ∀ x ∈ A f ⁡ x ∈ C
3 2 anim2d ⊢ ∀ x ∈ A B ⊆ C → f Fn x | x ∈ A ∧ ∀ x ∈ A f ⁡ x ∈ B → f Fn x | x ∈ A ∧ ∀ x ∈ A f ⁡ x ∈ C
4 3 ss2abdv ⊢ ∀ x ∈ A B ⊆ C → f | f Fn x | x ∈ A ∧ ∀ x ∈ A f ⁡ x ∈ B ⊆ f | f Fn x | x ∈ A ∧ ∀ x ∈ A f ⁡ x ∈ C
5 df-ixp ⊢ ⨉ x ∈ A B = f | f Fn x | x ∈ A ∧ ∀ x ∈ A f ⁡ x ∈ B
6 df-ixp ⊢ ⨉ x ∈ A C = f | f Fn x | x ∈ A ∧ ∀ x ∈ A f ⁡ x ∈ C
7 4 5 6 3sstr4g ⊢ ∀ x ∈ A B ⊆ C → ⨉ x ∈ A B ⊆ ⨉ x ∈ A C