Theorem marypha2lem1

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

	Ref	Expression
Hypothesis	marypha2lem.t	|- T = U_ x e. A ( { x } X. ( F ` x ) )
Assertion	marypha2lem1	|- T C_ ( A X. U. ran F )

Proof

Step	Hyp	Ref	Expression
1		marypha2lem.t	|- T = U_ x e. A ( { x } X. ( F ` x ) )
2		iunss	|- ( U_ x e. A ( { x } X. ( F ` x ) ) C_ ( A X. U. ran F ) <-> A. x e. A ( { x } X. ( F ` x ) ) C_ ( A X. U. ran F ) )
3		snssi	|- ( x e. A -> { x } C_ A )
4		fvssunirn	|- ( F ` x ) C_ U. ran F
5		xpss12	|- ( ( { x } C_ A /\ ( F ` x ) C_ U. ran F ) -> ( { x } X. ( F ` x ) ) C_ ( A X. U. ran F ) )
6	3 4 5	sylancl	|- ( x e. A -> ( { x } X. ( F ` x ) ) C_ ( A X. U. ran F ) )
7	2 6	mprgbir	|- U_ x e. A ( { x } X. ( F ` x ) ) C_ ( A X. U. ran F )
8	1 7	eqsstri	|- T C_ ( A X. U. ran F )