Theorem qliftf

Description: The domain and codomain of the function F . (Contributed by Mario Carneiro, 23-Dec-2016) (Revised by AV, 3-Aug-2024)

	Ref	Expression
Hypotheses	qlift.1	$$⊢F=\mathrm{ran}\left(x\in X⟼⟨\left[x\right]R,A⟩\right)$$
	qlift.2	$$⊢\left(\phi \wedge x\in X\right)\to A\in Y$$
	qlift.3	$$⊢\phi \to R\mathrm{Er}X$$
	qlift.4	$$⊢\phi \to X\in V$$
Assertion	qliftf	$$⊢\phi \to \left(\mathrm{Fun}F\leftrightarrow F:X/R⟶Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		qlift.1	$$⊢F=\mathrm{ran}\left(x\in X⟼⟨\left[x\right]R,A⟩\right)$$
2		qlift.2	$$⊢\left(\phi \wedge x\in X\right)\to A\in Y$$
3		qlift.3	$$⊢\phi \to R\mathrm{Er}X$$
4		qlift.4	$$⊢\phi \to X\in V$$
5	1 2 3 4	qliftlem	$$⊢\left(\phi \wedge x\in X\right)\to \left[x\right]R\in \left(X/R\right)$$
6	1 5 2	fliftf	$$⊢\phi \to \left(\mathrm{Fun}F\leftrightarrow F:\mathrm{ran}\left(x\in X⟼\left[x\right]R\right)⟶Y\right)$$
7		df-qs	$$⊢X/R=\left\{y|\exists x\in Xy=\left[x\right]R\right\}$$
8		eqid	$$⊢\left(x\in X⟼\left[x\right]R\right)=\left(x\in X⟼\left[x\right]R\right)$$
9	8	rnmpt	$$⊢\mathrm{ran}\left(x\in X⟼\left[x\right]R\right)=\left\{y|\exists x\in Xy=\left[x\right]R\right\}$$
10	7 9	eqtr4i	$$⊢X/R=\mathrm{ran}\left(x\in X⟼\left[x\right]R\right)$$
11	10	a1i	$$⊢\phi \to X/R=\mathrm{ran}\left(x\in X⟼\left[x\right]R\right)$$
12	11	feq2d	$$⊢\phi \to \left(F:X/R⟶Y\leftrightarrow F:\mathrm{ran}\left(x\in X⟼\left[x\right]R\right)⟶Y\right)$$
13	6 12	bitr4d	$$⊢\phi \to \left(\mathrm{Fun}F\leftrightarrow F:X/R⟶Y\right)$$