Metamath Proof Explorer

Theorem cdlemk40

Description: TODO: fix comment. (Contributed by NM, 31-Jul-2013)

Ref Expression
Hypotheses cdlemk40.x 
|- X = ( iota_ z e. T ph )
cdlemk40.u 
|- U = ( g e. T |-> if ( F = N , g , X ) )
Assertion cdlemk40 
|- ( G e. T -> ( U ` G ) = if ( F = N , G , [_ G / g ]_ X ) )

Proof

Step Hyp Ref Expression
1 cdlemk40.x 
 |-  X = ( iota_ z e. T ph )
2 cdlemk40.u 
 |-  U = ( g e. T |-> if ( F = N , g , X ) )
3 vex 
 |-  g e. _V
4 riotaex 
 |-  ( iota_ z e. T ph ) e. _V
5 1 4 eqeltri 
 |-  X e. _V
6 3 5 ifex 
 |-  if ( F = N , g , X ) e. _V
7 6 csbex 
 |-  [_ G / g ]_ if ( F = N , g , X ) e. _V
8 2 fvmpts 
 |-  ( ( G e. T /\ [_ G / g ]_ if ( F = N , g , X ) e. _V ) -> ( U ` G ) = [_ G / g ]_ if ( F = N , g , X ) )
9 7 8 mpan2 
 |-  ( G e. T -> ( U ` G ) = [_ G / g ]_ if ( F = N , g , X ) )
10 csbif 
 |-  [_ G / g ]_ if ( F = N , g , X ) = if ( [. G / g ]. F = N , [_ G / g ]_ g , [_ G / g ]_ X )
11 sbcg 
 |-  ( G e. T -> ( [. G / g ]. F = N <-> F = N ) )
12 csbvarg 
 |-  ( G e. T -> [_ G / g ]_ g = G )
13 11 12 ifbieq1d 
 |-  ( G e. T -> if ( [. G / g ]. F = N , [_ G / g ]_ g , [_ G / g ]_ X ) = if ( F = N , G , [_ G / g ]_ X ) )
14 10 13 eqtrid 
 |-  ( G e. T -> [_ G / g ]_ if ( F = N , g , X ) = if ( F = N , G , [_ G / g ]_ X ) )
15 9 14 eqtrd 
 |-  ( G e. T -> ( U ` G ) = if ( F = N , G , [_ G / g ]_ X ) )