Theorem fliftfuns

Description: The function F is the unique function defined by FA = B , provided that the well-definedness condition holds. (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	fliftfuns	$$⊢\phi \to \left(\mathrm{Fun}F\leftrightarrow \forall y\in X\forall z\in X\left(⦋y/x⦌A=⦋z/x⦌A\to ⦋y/x⦌B=⦋z/x⦌B\right)\right)$$

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		nfcv	$$⊢\underset{\_}{Ⅎ}y⟨A,B⟩$$
5		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌A$$
6		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌B$$
7	5 6	nfop	$$⊢\underset{\_}{Ⅎ}x⟨⦋y/x⦌A,⦋y/x⦌B⟩$$
8		csbeq1a	$$⊢x=y\to A=⦋y/x⦌A$$
9		csbeq1a	$$⊢x=y\to B=⦋y/x⦌B$$
10	8 9	opeq12d	$$⊢x=y\to ⟨A,B⟩=⟨⦋y/x⦌A,⦋y/x⦌B⟩$$
11	4 7 10	cbvmpt	$$⊢\left(x\in X⟼⟨A,B⟩\right)=\left(y\in X⟼⟨⦋y/x⦌A,⦋y/x⦌B⟩\right)$$
12	11	rneqi	$$⊢\mathrm{ran}\left(x\in X⟼⟨A,B⟩\right)=\mathrm{ran}\left(y\in X⟼⟨⦋y/x⦌A,⦋y/x⦌B⟩\right)$$
13	1 12	eqtri	$$⊢F=\mathrm{ran}\left(y\in X⟼⟨⦋y/x⦌A,⦋y/x⦌B⟩\right)$$
14	2	ralrimiva	$$⊢\phi \to \forall x\in XA\in R$$
15	5	nfel1	$$⊢Ⅎx⦋y/x⦌A\in R$$
16	8	eleq1d	$$⊢x=y\to \left(A\in R\leftrightarrow ⦋y/x⦌A\in R\right)$$
17	15 16	rspc	$$⊢y\in X\to \left(\forall x\in XA\in R\to ⦋y/x⦌A\in R\right)$$
18	14 17	mpan9	$$⊢\left(\phi \wedge y\in X\right)\to ⦋y/x⦌A\in R$$
19	3	ralrimiva	$$⊢\phi \to \forall x\in XB\in S$$
20	6	nfel1	$$⊢Ⅎx⦋y/x⦌B\in S$$
21	9	eleq1d	$$⊢x=y\to \left(B\in S\leftrightarrow ⦋y/x⦌B\in S\right)$$
22	20 21	rspc	$$⊢y\in X\to \left(\forall x\in XB\in S\to ⦋y/x⦌B\in S\right)$$
23	19 22	mpan9	$$⊢\left(\phi \wedge y\in X\right)\to ⦋y/x⦌B\in S$$
24		csbeq1	$$⊢y=z\to ⦋y/x⦌A=⦋z/x⦌A$$
25		csbeq1	$$⊢y=z\to ⦋y/x⦌B=⦋z/x⦌B$$
26	13 18 23 24 25	fliftfun	$$⊢\phi \to \left(\mathrm{Fun}F\leftrightarrow \forall y\in X\forall z\in X\left(⦋y/x⦌A=⦋z/x⦌A\to ⦋y/x⦌B=⦋z/x⦌B\right)\right)$$