marypha2lem1

Description: Lemma for marypha2 . Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015)

		Ref	Expression
	Hypothesis	marypha2lem.t	$⊢ T = ⋃_{x \in A} (\{x\} \times F (x))$
	Assertion	marypha2lem1	$⊢ T \subseteq A \times ⋃ ran F$

Step	Hyp	Ref	Expression
1		marypha2lem.t	$⊢ T = ⋃_{x \in A} (\{x\} \times F (x))$
2		iunss	$⊢ ⋃_{x \in A} (\{x\} \times F (x)) \subseteq A \times ⋃ ran F \leftrightarrow \forall x \in A \{x\} \times F (x) \subseteq A \times ⋃ ran F$
3		snssi	$⊢ x \in A \to \{x\} \subseteq A$
4		fvssunirn	$⊢ F (x) \subseteq ⋃ ran F$
5		xpss12	$⊢ (\{x\} \subseteq A \land F (x) \subseteq ⋃ ran F) \to \{x\} \times F (x) \subseteq A \times ⋃ ran F$
6	3 4 5	sylancl	$⊢ x \in A \to \{x\} \times F (x) \subseteq A \times ⋃ ran F$
7	2 6	mprgbir	$⊢ ⋃_{x \in A} (\{x\} \times F (x)) \subseteq A \times ⋃ ran F$
8	1 7	eqsstri	$⊢ T \subseteq A \times ⋃ ran F$

Metamath Proof Explorer