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