Theorem qliftfuns

Description: The function F is the unique function defined by F[ x ] = A , provided that the well-definedness condition holds. (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	qliftfuns	$$⊢\phi \to \left(\mathrm{Fun}F\leftrightarrow \forall y\forall z\left(yRz\to ⦋y/x⦌A=⦋z/x⦌A\right)\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		nfcv	$$⊢\underset{\_}{Ⅎ}y⟨\left[x\right]R,A⟩$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}x\left[y\right]R$$
7		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌A$$
8	6 7	nfop	$$⊢\underset{\_}{Ⅎ}x⟨\left[y\right]R,⦋y/x⦌A⟩$$
9		eceq1	$$⊢x=y\to \left[x\right]R=\left[y\right]R$$
10		csbeq1a	$$⊢x=y\to A=⦋y/x⦌A$$
11	9 10	opeq12d	$$⊢x=y\to ⟨\left[x\right]R,A⟩=⟨\left[y\right]R,⦋y/x⦌A⟩$$
12	5 8 11	cbvmpt	$$⊢\left(x\in X⟼⟨\left[x\right]R,A⟩\right)=\left(y\in X⟼⟨\left[y\right]R,⦋y/x⦌A⟩\right)$$
13	12	rneqi	$$⊢\mathrm{ran}\left(x\in X⟼⟨\left[x\right]R,A⟩\right)=\mathrm{ran}\left(y\in X⟼⟨\left[y\right]R,⦋y/x⦌A⟩\right)$$
14	1 13	eqtri	$$⊢F=\mathrm{ran}\left(y\in X⟼⟨\left[y\right]R,⦋y/x⦌A⟩\right)$$
15	2	ralrimiva	$$⊢\phi \to \forall x\in XA\in Y$$
16	7	nfel1	$$⊢Ⅎx⦋y/x⦌A\in Y$$
17	10	eleq1d	$$⊢x=y\to \left(A\in Y\leftrightarrow ⦋y/x⦌A\in Y\right)$$
18	16 17	rspc	$$⊢y\in X\to \left(\forall x\in XA\in Y\to ⦋y/x⦌A\in Y\right)$$
19	15 18	mpan9	$$⊢\left(\phi \wedge y\in X\right)\to ⦋y/x⦌A\in Y$$
20		csbeq1	$$⊢y=z\to ⦋y/x⦌A=⦋z/x⦌A$$
21	14 19 3 4 20	qliftfun	$$⊢\phi \to \left(\mathrm{Fun}F\leftrightarrow \forall y\forall z\left(yRz\to ⦋y/x⦌A=⦋z/x⦌A\right)\right)$$