| Step |
Hyp |
Ref |
Expression |
| 1 |
|
unxpdomlem1.1 |
|- F = ( x e. ( a u. b ) |-> G ) |
| 2 |
|
unxpdomlem1.2 |
|- G = if ( x e. a , <. x , if ( x = m , t , s ) >. , <. if ( x = t , n , m ) , x >. ) |
| 3 |
|
elequ1 |
|- ( x = z -> ( x e. a <-> z e. a ) ) |
| 4 |
|
opeq1 |
|- ( x = z -> <. x , if ( x = m , t , s ) >. = <. z , if ( x = m , t , s ) >. ) |
| 5 |
|
equequ1 |
|- ( x = z -> ( x = m <-> z = m ) ) |
| 6 |
5
|
ifbid |
|- ( x = z -> if ( x = m , t , s ) = if ( z = m , t , s ) ) |
| 7 |
6
|
opeq2d |
|- ( x = z -> <. z , if ( x = m , t , s ) >. = <. z , if ( z = m , t , s ) >. ) |
| 8 |
4 7
|
eqtrd |
|- ( x = z -> <. x , if ( x = m , t , s ) >. = <. z , if ( z = m , t , s ) >. ) |
| 9 |
|
equequ1 |
|- ( x = z -> ( x = t <-> z = t ) ) |
| 10 |
9
|
ifbid |
|- ( x = z -> if ( x = t , n , m ) = if ( z = t , n , m ) ) |
| 11 |
10
|
opeq1d |
|- ( x = z -> <. if ( x = t , n , m ) , x >. = <. if ( z = t , n , m ) , x >. ) |
| 12 |
|
opeq2 |
|- ( x = z -> <. if ( z = t , n , m ) , x >. = <. if ( z = t , n , m ) , z >. ) |
| 13 |
11 12
|
eqtrd |
|- ( x = z -> <. if ( x = t , n , m ) , x >. = <. if ( z = t , n , m ) , z >. ) |
| 14 |
3 8 13
|
ifbieq12d |
|- ( x = z -> if ( x e. a , <. x , if ( x = m , t , s ) >. , <. if ( x = t , n , m ) , x >. ) = if ( z e. a , <. z , if ( z = m , t , s ) >. , <. if ( z = t , n , m ) , z >. ) ) |
| 15 |
2 14
|
syl5eq |
|- ( x = z -> G = if ( z e. a , <. z , if ( z = m , t , s ) >. , <. if ( z = t , n , m ) , z >. ) ) |
| 16 |
|
opex |
|- <. z , if ( z = m , t , s ) >. e. _V |
| 17 |
|
opex |
|- <. if ( z = t , n , m ) , z >. e. _V |
| 18 |
16 17
|
ifex |
|- if ( z e. a , <. z , if ( z = m , t , s ) >. , <. if ( z = t , n , m ) , z >. ) e. _V |
| 19 |
15 1 18
|
fvmpt |
|- ( z e. ( a u. b ) -> ( F ` z ) = if ( z e. a , <. z , if ( z = m , t , s ) >. , <. if ( z = t , n , m ) , z >. ) ) |