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 = ran ( x e. X |-> <. [ x ] R , A >. )
	qlift.2	|- ( ( ph /\ x e. X ) -> A e. Y )
	qlift.3	|- ( ph -> R Er X )
	qlift.4	|- ( ph -> X e. V )
Assertion	qliftfuns	|- ( ph -> ( Fun F <-> A. y A. z ( y R z -> [_ y / x ]_ A = [_ z / x ]_ A ) ) )

Proof

Step	Hyp	Ref	Expression
1		qlift.1	|- F = ran ( x e. X |-> <. [ x ] R , A >. )
2		qlift.2	|- ( ( ph /\ x e. X ) -> A e. Y )
3		qlift.3	|- ( ph -> R Er X )
4		qlift.4	|- ( ph -> X e. V )
5		nfcv	|- F/_ y <. [ x ] R , A >.
6		nfcv	|- F/_ x [ y ] R
7		nfcsb1v	|- F/_ x [_ y / x ]_ A
8	6 7	nfop	|- F/_ x <. [ y ] R , [_ y / x ]_ A >.
9		eceq1	|- ( x = y -> [ x ] R = [ y ] R )
10		csbeq1a	|- ( x = y -> A = [_ y / x ]_ A )
11	9 10	opeq12d	|- ( x = y -> <. [ x ] R , A >. = <. [ y ] R , [_ y / x ]_ A >. )
12	5 8 11	cbvmpt	|- ( x e. X |-> <. [ x ] R , A >. ) = ( y e. X |-> <. [ y ] R , [_ y / x ]_ A >. )
13	12	rneqi	|- ran ( x e. X |-> <. [ x ] R , A >. ) = ran ( y e. X |-> <. [ y ] R , [_ y / x ]_ A >. )
14	1 13	eqtri	|- F = ran ( y e. X |-> <. [ y ] R , [_ y / x ]_ A >. )
15	2	ralrimiva	|- ( ph -> A. x e. X A e. Y )
16	7	nfel1	|- F/ x [_ y / x ]_ A e. Y
17	10	eleq1d	|- ( x = y -> ( A e. Y <-> [_ y / x ]_ A e. Y ) )
18	16 17	rspc	|- ( y e. X -> ( A. x e. X A e. Y -> [_ y / x ]_ A e. Y ) )
19	15 18	mpan9	|- ( ( ph /\ y e. X ) -> [_ y / x ]_ A e. Y )
20		csbeq1	|- ( y = z -> [_ y / x ]_ A = [_ z / x ]_ A )
21	14 19 3 4 20	qliftfun	|- ( ph -> ( Fun F <-> A. y A. z ( y R z -> [_ y / x ]_ A = [_ z / x ]_ A ) ) )