Theorem fliftrel

Description: F , a function lift, is a subset of R X. S . (Contributed by Mario Carneiro, 23-Dec-2016)

	Ref	Expression
Hypotheses	flift.1	|- F = ran ( x e. X |-> <. A , B >. )
	flift.2	|- ( ( ph /\ x e. X ) -> A e. R )
	flift.3	|- ( ( ph /\ x e. X ) -> B e. S )
Assertion	fliftrel	|- ( ph -> F C_ ( R X. S ) )

Proof

Step	Hyp	Ref	Expression
1		flift.1	|- F = ran ( x e. X |-> <. A , B >. )
2		flift.2	|- ( ( ph /\ x e. X ) -> A e. R )
3		flift.3	|- ( ( ph /\ x e. X ) -> B e. S )
4	2 3	opelxpd	|- ( ( ph /\ x e. X ) -> <. A , B >. e. ( R X. S ) )
5	4	fmpttd	|- ( ph -> ( x e. X |-> <. A , B >. ) : X --> ( R X. S ) )
6	5	frnd	|- ( ph -> ran ( x e. X |-> <. A , B >. ) C_ ( R X. S ) )
7	1 6	eqsstrid	|- ( ph -> F C_ ( R X. S ) )