This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qliftf

Description: The domain and codomain 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 ) )