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