Metamath Proof Explorer

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 = ran ( x e. X |-> <. A , B >. )
flift.2 
|- ( ( ph /\ x e. X ) -> A e. R )
flift.3 
|- ( ( ph /\ x e. X ) -> B e. S )
Assertion fliftfuns 
|- ( ph -> ( Fun F <-> A. y e. X A. z e. X ( [_ y / x ]_ A = [_ z / x ]_ A -> [_ y / x ]_ B = [_ z / x ]_ B ) ) )

Proof

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