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=\mathrm{ran}\left(x\in X⟼⟨A,B⟩\right)$$
	flift.2	$$⊢\left(\phi \wedge x\in X\right)\to A\in R$$
	flift.3	$$⊢\left(\phi \wedge x\in X\right)\to B\in S$$
Assertion	fliftrel	$$⊢\phi \to F\subseteq R\times S$$

Proof

Step	Hyp	Ref	Expression
1		flift.1	$$⊢F=\mathrm{ran}\left(x\in X⟼⟨A,B⟩\right)$$
2		flift.2	$$⊢\left(\phi \wedge x\in X\right)\to A\in R$$
3		flift.3	$$⊢\left(\phi \wedge x\in X\right)\to B\in S$$
4	2 3	opelxpd	$$⊢\left(\phi \wedge x\in X\right)\to ⟨A,B⟩\in \left(R\times S\right)$$
5	4	fmpttd	$$⊢\phi \to \left(x\in X⟼⟨A,B⟩\right):X⟶R\times S$$
6	5	frnd	$$⊢\phi \to \mathrm{ran}\left(x\in X⟼⟨A,B⟩\right)\subseteq R\times S$$
7	1 6	eqsstrid	$$⊢\phi \to F\subseteq R\times S$$