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

Metamath Proof Explorer

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 ) ) )