This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑥 ∈ 𝐴 𝐵 ⊆ X 𝑥 ∈ 𝐴 𝐶 )

Proof

Step Hyp Ref Expression
1 ssel ⊢ ( 𝐵 ⊆ 𝐶 → ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 → ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) )
2 1 ral2imi ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 → ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) )
3 2 anim2d ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ( ( 𝑓 Fn { 𝑥 ∣ 𝑥 ∈ 𝐴 } ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) → ( 𝑓 Fn { 𝑥 ∣ 𝑥 ∈ 𝐴 } ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) )
4 3 ss2abdv ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → { 𝑓 ∣ ( 𝑓 Fn { 𝑥 ∣ 𝑥 ∈ 𝐴 } ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) } ⊆ { 𝑓 ∣ ( 𝑓 Fn { 𝑥 ∣ 𝑥 ∈ 𝐴 } ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) } )
5 df-ixp ⊢ X 𝑥 ∈ 𝐴 𝐵 = { 𝑓 ∣ ( 𝑓 Fn { 𝑥 ∣ 𝑥 ∈ 𝐴 } ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) }
6 df-ixp ⊢ X 𝑥 ∈ 𝐴 𝐶 = { 𝑓 ∣ ( 𝑓 Fn { 𝑥 ∣ 𝑥 ∈ 𝐴 } ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) }
7 4 5 6 3sstr4g ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → X 𝑥 ∈ 𝐴 𝐵 ⊆ X 𝑥 ∈ 𝐴 𝐶 )