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

Metamath Proof Explorer

Theorem unxpdomlem1

Description: Lemma for unxpdom . (Trivial substitution proof.) (Contributed by Mario Carneiro, 13-Jan-2013)

Ref Expression
Hypotheses unxpdomlem1.1 
|- F = ( x e. ( a u. b ) |-> G )
unxpdomlem1.2 
|- G = if ( x e. a , <. x , if ( x = m , t , s ) >. , <. if ( x = t , n , m ) , x >. )
Assertion unxpdomlem1 
|- ( z e. ( a u. b ) -> ( F ` z ) = if ( z e. a , <. z , if ( z = m , t , s ) >. , <. if ( z = t , n , m ) , z >. ) )

Proof

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 eqtrid 
 |-  ( 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 >. ) )