Theorem qliftf

Description: The domain and range of the function F . (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	qliftf	|- ( ph -> ( Fun F <-> F : ( X /. R ) --> Y ) )

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	1 2 3 4	qliftlem	|- ( ( ph /\ x e. X ) -> [ x ] R e. ( X /. R ) )
6	1 5 2	fliftf	|- ( ph -> ( Fun F <-> F : ran ( x e. X |-> [ x ] R ) --> Y ) )
7		df-qs	|- ( X /. R ) = { y | E. x e. X y = [ x ] R }
8		eqid	|- ( x e. X |-> [ x ] R ) = ( x e. X |-> [ x ] R )
9	8	rnmpt	|- ran ( x e. X |-> [ x ] R ) = { y | E. x e. X y = [ x ] R }
10	7 9	eqtr4i	|- ( X /. R ) = ran ( x e. X |-> [ x ] R )
11	10	a1i	|- ( ph -> ( X /. R ) = ran ( x e. X |-> [ x ] R ) )
12	11	feq2d	|- ( ph -> ( F : ( X /. R ) --> Y <-> F : ran ( x e. X |-> [ x ] R ) --> Y ) )
13	6 12	bitr4d	|- ( ph -> ( Fun F <-> F : ( X /. R ) --> Y ) )