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	$⊢ \forall x \in A B \subseteq C \to \underset{x \in A}{⨉} B \subseteq \underset{x \in A}{⨉} C$

Step	Hyp	Ref	Expression
1		ssel	$⊢ B \subseteq C \to (f (x) \in B \to f (x) \in C)$
2	1	ral2imi	$⊢ \forall x \in A B \subseteq C \to (\forall x \in A f (x) \in B \to \forall x \in A f (x) \in C)$
3	2	anim2d	$⊢ \forall x \in A B \subseteq C \to ((f Fn \{x \| x \in A\} \land \forall x \in A f (x) \in B) \to (f Fn \{x \| x \in A\} \land \forall x \in A f (x) \in C))$
4	3	ss2abdv	$⊢ \forall x \in A B \subseteq C \to \{f \| (f Fn \{x \| x \in A\} \land \forall x \in A f (x) \in B)\} \subseteq \{f \| (f Fn \{x \| x \in A\} \land \forall x \in A f (x) \in C)\}$
5		df-ixp	$⊢ \underset{x \in A}{⨉} B = \{f \| (f Fn \{x \| x \in A\} \land \forall x \in A f (x) \in B)\}$
6		df-ixp	$⊢ \underset{x \in A}{⨉} C = \{f \| (f Fn \{x \| x \in A\} \land \forall x \in A f (x) \in C)\}$
7	4 5 6	3sstr4g	$⊢ \forall x \in A B \subseteq C \to \underset{x \in A}{⨉} B \subseteq \underset{x \in A}{⨉} C$

Metamath Proof Explorer