Metamath Proof Explorer

Theorem unxpdomlem2

Description: Lemma for unxpdom . (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 >. )
unxpdomlem2.1 
|- ( ph -> w e. ( a u. b ) )
unxpdomlem2.2 
|- ( ph -> -. m = n )
unxpdomlem2.3 
|- ( ph -> -. s = t )
Assertion unxpdomlem2 
|- ( ( ph /\ ( z e. a /\ -. w e. a ) ) -> -. ( F ` z ) = ( F ` w ) )

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 unxpdomlem2.1 
 |-  ( ph -> w e. ( a u. b ) )
4 unxpdomlem2.2 
 |-  ( ph -> -. m = n )
5 unxpdomlem2.3 
 |-  ( ph -> -. s = t )
6 5 adantr 
 |-  ( ( ph /\ ( z e. a /\ -. w e. a ) ) -> -. s = t )
7 elun1 
 |-  ( z e. a -> z e. ( a u. b ) )
8 7 ad2antrl 
 |-  ( ( ph /\ ( z e. a /\ -. w e. a ) ) -> z e. ( a u. b ) )
9 1 2 unxpdomlem1 
 |-  ( z e. ( a u. b ) -> ( F ` z ) = if ( z e. a , <. z , if ( z = m , t , s ) >. , <. if ( z = t , n , m ) , z >. ) )
10 8 9 syl 
 |-  ( ( ph /\ ( z e. a /\ -. w e. a ) ) -> ( F ` z ) = if ( z e. a , <. z , if ( z = m , t , s ) >. , <. if ( z = t , n , m ) , z >. ) )
11 iftrue 
 |-  ( z e. a -> if ( z e. a , <. z , if ( z = m , t , s ) >. , <. if ( z = t , n , m ) , z >. ) = <. z , if ( z = m , t , s ) >. )
12 11 ad2antrl 
 |-  ( ( ph /\ ( z e. a /\ -. w e. a ) ) -> if ( z e. a , <. z , if ( z = m , t , s ) >. , <. if ( z = t , n , m ) , z >. ) = <. z , if ( z = m , t , s ) >. )
13 10 12 eqtrd 
 |-  ( ( ph /\ ( z e. a /\ -. w e. a ) ) -> ( F ` z ) = <. z , if ( z = m , t , s ) >. )
14 3 adantr 
 |-  ( ( ph /\ ( z e. a /\ -. w e. a ) ) -> w e. ( a u. b ) )
15 1 2 unxpdomlem1 
 |-  ( w e. ( a u. b ) -> ( F ` w ) = if ( w e. a , <. w , if ( w = m , t , s ) >. , <. if ( w = t , n , m ) , w >. ) )
16 14 15 syl 
 |-  ( ( ph /\ ( z e. a /\ -. w e. a ) ) -> ( F ` w ) = if ( w e. a , <. w , if ( w = m , t , s ) >. , <. if ( w = t , n , m ) , w >. ) )
17 iffalse 
 |-  ( -. w e. a -> if ( w e. a , <. w , if ( w = m , t , s ) >. , <. if ( w = t , n , m ) , w >. ) = <. if ( w = t , n , m ) , w >. )
18 17 ad2antll 
 |-  ( ( ph /\ ( z e. a /\ -. w e. a ) ) -> if ( w e. a , <. w , if ( w = m , t , s ) >. , <. if ( w = t , n , m ) , w >. ) = <. if ( w = t , n , m ) , w >. )
19 16 18 eqtrd 
 |-  ( ( ph /\ ( z e. a /\ -. w e. a ) ) -> ( F ` w ) = <. if ( w = t , n , m ) , w >. )
20 13 19 eqeq12d 
 |-  ( ( ph /\ ( z e. a /\ -. w e. a ) ) -> ( ( F ` z ) = ( F ` w ) <-> <. z , if ( z = m , t , s ) >. = <. if ( w = t , n , m ) , w >. ) )
21 20 biimpa 
 |-  ( ( ( ph /\ ( z e. a /\ -. w e. a ) ) /\ ( F ` z ) = ( F ` w ) ) -> <. z , if ( z = m , t , s ) >. = <. if ( w = t , n , m ) , w >. )
22 vex 
 |-  z e. _V
23 vex 
 |-  t e. _V
24 vex 
 |-  s e. _V
25 23 24 ifex 
 |-  if ( z = m , t , s ) e. _V
26 22 25 opth 
 |-  ( <. z , if ( z = m , t , s ) >. = <. if ( w = t , n , m ) , w >. <-> ( z = if ( w = t , n , m ) /\ if ( z = m , t , s ) = w ) )
27 21 26 sylib 
 |-  ( ( ( ph /\ ( z e. a /\ -. w e. a ) ) /\ ( F ` z ) = ( F ` w ) ) -> ( z = if ( w = t , n , m ) /\ if ( z = m , t , s ) = w ) )
28 27 simprd 
 |-  ( ( ( ph /\ ( z e. a /\ -. w e. a ) ) /\ ( F ` z ) = ( F ` w ) ) -> if ( z = m , t , s ) = w )
29 iftrue 
 |-  ( z = m -> if ( z = m , t , s ) = t )
30 28 eqeq1d 
 |-  ( ( ( ph /\ ( z e. a /\ -. w e. a ) ) /\ ( F ` z ) = ( F ` w ) ) -> ( if ( z = m , t , s ) = t <-> w = t ) )
31 29 30 syl5ib 
 |-  ( ( ( ph /\ ( z e. a /\ -. w e. a ) ) /\ ( F ` z ) = ( F ` w ) ) -> ( z = m -> w = t ) )
32 iftrue 
 |-  ( w = t -> if ( w = t , n , m ) = n )
33 27 simpld 
 |-  ( ( ( ph /\ ( z e. a /\ -. w e. a ) ) /\ ( F ` z ) = ( F ` w ) ) -> z = if ( w = t , n , m ) )
34 33 eqeq1d 
 |-  ( ( ( ph /\ ( z e. a /\ -. w e. a ) ) /\ ( F ` z ) = ( F ` w ) ) -> ( z = n <-> if ( w = t , n , m ) = n ) )
35 32 34 syl5ibr 
 |-  ( ( ( ph /\ ( z e. a /\ -. w e. a ) ) /\ ( F ` z ) = ( F ` w ) ) -> ( w = t -> z = n ) )
36 31 35 syld 
 |-  ( ( ( ph /\ ( z e. a /\ -. w e. a ) ) /\ ( F ` z ) = ( F ` w ) ) -> ( z = m -> z = n ) )
37 4 ad2antrr 
 |-  ( ( ( ph /\ ( z e. a /\ -. w e. a ) ) /\ ( F ` z ) = ( F ` w ) ) -> -. m = n )
38 equequ1 
 |-  ( z = m -> ( z = n <-> m = n ) )
39 38 notbid 
 |-  ( z = m -> ( -. z = n <-> -. m = n ) )
40 37 39 syl5ibrcom 
 |-  ( ( ( ph /\ ( z e. a /\ -. w e. a ) ) /\ ( F ` z ) = ( F ` w ) ) -> ( z = m -> -. z = n ) )
41 36 40 pm2.65d 
 |-  ( ( ( ph /\ ( z e. a /\ -. w e. a ) ) /\ ( F ` z ) = ( F ` w ) ) -> -. z = m )
42 41 iffalsed 
 |-  ( ( ( ph /\ ( z e. a /\ -. w e. a ) ) /\ ( F ` z ) = ( F ` w ) ) -> if ( z = m , t , s ) = s )
43 iffalse 
 |-  ( -. w = t -> if ( w = t , n , m ) = m )
44 33 eqeq1d 
 |-  ( ( ( ph /\ ( z e. a /\ -. w e. a ) ) /\ ( F ` z ) = ( F ` w ) ) -> ( z = m <-> if ( w = t , n , m ) = m ) )
45 43 44 syl5ibr 
 |-  ( ( ( ph /\ ( z e. a /\ -. w e. a ) ) /\ ( F ` z ) = ( F ` w ) ) -> ( -. w = t -> z = m ) )
46 41 45 mt3d 
 |-  ( ( ( ph /\ ( z e. a /\ -. w e. a ) ) /\ ( F ` z ) = ( F ` w ) ) -> w = t )
47 28 42 46 3eqtr3d 
 |-  ( ( ( ph /\ ( z e. a /\ -. w e. a ) ) /\ ( F ` z ) = ( F ` w ) ) -> s = t )
48 6 47 mtand 
 |-  ( ( ph /\ ( z e. a /\ -. w e. a ) ) -> -. ( F ` z ) = ( F ` w ) )