Theorem qliftfund

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$$
	qliftfun.4	$$⊢x=y\to A=B$$
	qliftfund.6	$$⊢\left(\phi \wedge xRy\right)\to A=B$$
Assertion	qliftfund	$$⊢\phi \to \mathrm{Fun}F$$

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		qliftfun.4	$$⊢x=y\to A=B$$
6		qliftfund.6	$$⊢\left(\phi \wedge xRy\right)\to A=B$$
7	6	ex	$$⊢\phi \to \left(xRy\to A=B\right)$$
8	7	alrimivv	$$⊢\phi \to \forall x\forall y\left(xRy\to A=B\right)$$
9	1 2 3 4 5	qliftfun	$$⊢\phi \to \left(\mathrm{Fun}F\leftrightarrow \forall x\forall y\left(xRy\to A=B\right)\right)$$
10	8 9	mpbird	$$⊢\phi \to \mathrm{Fun}F$$