Users' Mathboxes Mathbox for ML < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  finxpreclem2 Structured version   Visualization version   Unicode version

Theorem finxpreclem2 31794
Description: Lemma for  ^^ ^^ recursion theorems. (Contributed by ML, 17-Oct-2020.)
Assertion
Ref Expression
finxpreclem2  |-  ( ( X  e.  _V  /\  -.  X  e.  U
)  ->  -.  (/)  =  ( ( n  e.  om ,  x  e.  _V  |->  if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  x
) >. ,  <. n ,  x >. ) ) ) `
 <. 1o ,  X >. ) )
Distinct variable groups:    U, n, x    n, X, x

Proof of Theorem finxpreclem2
StepHypRef Expression
1 nfv 1763 . . . . . 6  |-  F/ x
( X  e.  _V  /\ 
-.  X  e.  U
)
2 nfmpt22 6364 . . . . . . . 8  |-  F/_ x
( n  e.  om ,  x  e.  _V  |->  if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  x
) >. ,  <. n ,  x >. ) ) )
3 nfcv 2594 . . . . . . . 8  |-  F/_ x <. 1o ,  X >.
42, 3nffv 5877 . . . . . . 7  |-  F/_ x
( ( n  e. 
om ,  x  e. 
_V  |->  if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V 
X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. ) ) ) `
 <. 1o ,  X >. )
5 nfcv 2594 . . . . . . 7  |-  F/_ x (/)
64, 5nfne 2725 . . . . . 6  |-  F/ x
( ( n  e. 
om ,  x  e. 
_V  |->  if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V 
X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. ) ) ) `
 <. 1o ,  X >. )  =/=  (/)
71, 6nfim 2005 . . . . 5  |-  F/ x
( ( X  e. 
_V  /\  -.  X  e.  U )  ->  (
( n  e.  om ,  x  e.  _V  |->  if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  x
) >. ,  <. n ,  x >. ) ) ) `
 <. 1o ,  X >. )  =/=  (/) )
8 nfv 1763 . . . . . . 7  |-  F/ n  x  =  X
9 nfv 1763 . . . . . . . 8  |-  F/ n
( X  e.  _V  /\ 
-.  X  e.  U
)
10 nfmpt21 6363 . . . . . . . . . 10  |-  F/_ n
( n  e.  om ,  x  e.  _V  |->  if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  x
) >. ,  <. n ,  x >. ) ) )
11 nfcv 2594 . . . . . . . . . 10  |-  F/_ n <. 1o ,  X >.
1210, 11nffv 5877 . . . . . . . . 9  |-  F/_ n
( ( n  e. 
om ,  x  e. 
_V  |->  if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V 
X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. ) ) ) `
 <. 1o ,  X >. )
13 nfcv 2594 . . . . . . . . 9  |-  F/_ n (/)
1412, 13nfne 2725 . . . . . . . 8  |-  F/ n
( ( n  e. 
om ,  x  e. 
_V  |->  if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V 
X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. ) ) ) `
 <. 1o ,  X >. )  =/=  (/)
159, 14nfim 2005 . . . . . . 7  |-  F/ n
( ( X  e. 
_V  /\  -.  X  e.  U )  ->  (
( n  e.  om ,  x  e.  _V  |->  if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  x
) >. ,  <. n ,  x >. ) ) ) `
 <. 1o ,  X >. )  =/=  (/) )
168, 15nfim 2005 . . . . . 6  |-  F/ n
( x  =  X  ->  ( ( X  e.  _V  /\  -.  X  e.  U )  ->  ( ( n  e. 
om ,  x  e. 
_V  |->  if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V 
X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. ) ) ) `
 <. 1o ,  X >. )  =/=  (/) ) )
17 1onn 7345 . . . . . . 7  |-  1o  e.  om
1817elexi 3057 . . . . . 6  |-  1o  e.  _V
19 df-ov 6298 . . . . . . . . . 10  |-  ( 1o ( n  e.  om ,  x  e.  _V  |->  if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  x
) >. ,  <. n ,  x >. ) ) ) X )  =  ( ( n  e.  om ,  x  e.  _V  |->  if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  x
) >. ,  <. n ,  x >. ) ) ) `
 <. 1o ,  X >. )
20 0ex 4538 . . . . . . . . . . . . . . . 16  |-  (/)  e.  _V
21 opex 4667 . . . . . . . . . . . . . . . . 17  |-  <. U. n ,  ( 1st `  x
) >.  e.  _V
22 opex 4667 . . . . . . . . . . . . . . . . 17  |-  <. n ,  x >.  e.  _V
2321, 22ifex 3951 . . . . . . . . . . . . . . . 16  |-  if ( x  e.  ( _V 
X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. )  e.  _V
2420, 23ifex 3951 . . . . . . . . . . . . . . 15  |-  if ( ( n  =  1o 
/\  x  e.  U
) ,  (/) ,  if ( x  e.  ( _V  X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. ) )  e. 
_V
2524csbex 4541 . . . . . . . . . . . . . 14  |-  [_ X  /  x ]_ if ( ( n  =  1o 
/\  x  e.  U
) ,  (/) ,  if ( x  e.  ( _V  X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. ) )  e. 
_V
2625csbex 4541 . . . . . . . . . . . . 13  |-  [_ 1o  /  n ]_ [_ X  /  x ]_ if ( ( n  =  1o 
/\  x  e.  U
) ,  (/) ,  if ( x  e.  ( _V  X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. ) )  e. 
_V
27 eqid 2453 . . . . . . . . . . . . . 14  |-  ( n  e.  om ,  x  e.  _V  |->  if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V 
X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. ) ) )  =  ( n  e. 
om ,  x  e. 
_V  |->  if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V 
X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. ) ) )
2827ovmpt2s 6425 . . . . . . . . . . . . 13  |-  ( ( 1o  e.  om  /\  X  e.  _V  /\  [_ 1o  /  n ]_ [_ X  /  x ]_ if ( ( n  =  1o 
/\  x  e.  U
) ,  (/) ,  if ( x  e.  ( _V  X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. ) )  e. 
_V )  ->  ( 1o ( n  e.  om ,  x  e.  _V  |->  if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  x
) >. ,  <. n ,  x >. ) ) ) X )  =  [_ 1o  /  n ]_ [_ X  /  x ]_ if ( ( n  =  1o 
/\  x  e.  U
) ,  (/) ,  if ( x  e.  ( _V  X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. ) ) )
2917, 26, 28mp3an13 1357 . . . . . . . . . . . 12  |-  ( X  e.  _V  ->  ( 1o ( n  e.  om ,  x  e.  _V  |->  if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  x
) >. ,  <. n ,  x >. ) ) ) X )  =  [_ 1o  /  n ]_ [_ X  /  x ]_ if ( ( n  =  1o 
/\  x  e.  U
) ,  (/) ,  if ( x  e.  ( _V  X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. ) ) )
3029adantr 467 . . . . . . . . . . 11  |-  ( ( X  e.  _V  /\  ( -.  X  e.  U  /\  ( n  =  1o  /\  x  =  X ) ) )  ->  ( 1o ( n  e.  om ,  x  e.  _V  |->  if ( ( n  =  1o 
/\  x  e.  U
) ,  (/) ,  if ( x  e.  ( _V  X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. ) ) ) X )  =  [_ 1o  /  n ]_ [_ X  /  x ]_ if ( ( n  =  1o 
/\  x  e.  U
) ,  (/) ,  if ( x  e.  ( _V  X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. ) ) )
31 csbeq1a 3374 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  x
) >. ,  <. n ,  x >. ) )  = 
[_ X  /  x ]_ if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  x
) >. ,  <. n ,  x >. ) ) )
32 csbeq1a 3374 . . . . . . . . . . . . . . 15  |-  ( n  =  1o  ->  [_ X  /  x ]_ if ( ( n  =  1o 
/\  x  e.  U
) ,  (/) ,  if ( x  e.  ( _V  X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. ) )  = 
[_ 1o  /  n ]_ [_ X  /  x ]_ if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  x
) >. ,  <. n ,  x >. ) ) )
3331, 32sylan9eqr 2509 . . . . . . . . . . . . . 14  |-  ( ( n  =  1o  /\  x  =  X )  ->  if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  x
) >. ,  <. n ,  x >. ) )  = 
[_ 1o  /  n ]_ [_ X  /  x ]_ if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  x
) >. ,  <. n ,  x >. ) ) )
3433adantl 468 . . . . . . . . . . . . 13  |-  ( ( -.  X  e.  U  /\  ( n  =  1o 
/\  x  =  X ) )  ->  if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  x
) >. ,  <. n ,  x >. ) )  = 
[_ 1o  /  n ]_ [_ X  /  x ]_ if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  x
) >. ,  <. n ,  x >. ) ) )
35 eleq1 2519 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  X  ->  (
x  e.  U  <->  X  e.  U ) )
3635notbid 296 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  X  ->  ( -.  x  e.  U  <->  -.  X  e.  U ) )
3736biimprcd 229 . . . . . . . . . . . . . . . . . 18  |-  ( -.  X  e.  U  -> 
( x  =  X  ->  -.  x  e.  U ) )
38 pm3.14 505 . . . . . . . . . . . . . . . . . . 19  |-  ( ( -.  n  =  1o  \/  -.  x  e.  U )  ->  -.  ( n  =  1o  /\  x  e.  U ) )
3938olcs 397 . . . . . . . . . . . . . . . . . 18  |-  ( -.  x  e.  U  ->  -.  ( n  =  1o 
/\  x  e.  U
) )
4037, 39syl6 34 . . . . . . . . . . . . . . . . 17  |-  ( -.  X  e.  U  -> 
( x  =  X  ->  -.  ( n  =  1o  /\  x  e.  U ) ) )
41 iffalse 3892 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( n  =  1o 
/\  x  e.  U
)  ->  if (
( n  =  1o 
/\  x  e.  U
) ,  (/) ,  if ( x  e.  ( _V  X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. ) )  =  if ( x  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  x
) >. ,  <. n ,  x >. ) )
4240, 41syl6 34 . . . . . . . . . . . . . . . 16  |-  ( -.  X  e.  U  -> 
( x  =  X  ->  if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V 
X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. ) )  =  if ( x  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  x
) >. ,  <. n ,  x >. ) ) )
4342imp 431 . . . . . . . . . . . . . . 15  |-  ( ( -.  X  e.  U  /\  x  =  X
)  ->  if (
( n  =  1o 
/\  x  e.  U
) ,  (/) ,  if ( x  e.  ( _V  X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. ) )  =  if ( x  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  x
) >. ,  <. n ,  x >. ) )
44 ifeqor 3927 . . . . . . . . . . . . . . . . 17  |-  ( if ( x  e.  ( _V  X.  U ) ,  <. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. )  =  <. U. n ,  ( 1st `  x ) >.  \/  if ( x  e.  ( _V  X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. )  =  <. n ,  x >. )
45 vex 3050 . . . . . . . . . . . . . . . . . . . . . 22  |-  n  e. 
_V
4645uniex 6592 . . . . . . . . . . . . . . . . . . . . 21  |-  U. n  e.  _V
47 fvex 5880 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 1st `  x )  e.  _V
4846, 47opnzi 4677 . . . . . . . . . . . . . . . . . . . 20  |-  <. U. n ,  ( 1st `  x
) >.  =/=  (/)
4948neii 2628 . . . . . . . . . . . . . . . . . . 19  |-  -.  <. U. n ,  ( 1st `  x ) >.  =  (/)
50 eqeq1 2457 . . . . . . . . . . . . . . . . . . 19  |-  ( if ( x  e.  ( _V  X.  U ) ,  <. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. )  =  <. U. n ,  ( 1st `  x ) >.  ->  ( if ( x  e.  ( _V  X.  U ) ,  <. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. )  =  (/)  <->  <. U. n ,  ( 1st `  x ) >.  =  (/) ) )
5149, 50mtbiri 305 . . . . . . . . . . . . . . . . . 18  |-  ( if ( x  e.  ( _V  X.  U ) ,  <. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. )  =  <. U. n ,  ( 1st `  x ) >.  ->  -.  if ( x  e.  ( _V  X.  U ) ,  <. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. )  =  (/) )
52 vex 3050 . . . . . . . . . . . . . . . . . . . . 21  |-  x  e. 
_V
5345, 52opnzi 4677 . . . . . . . . . . . . . . . . . . . 20  |-  <. n ,  x >.  =/=  (/)
5453neii 2628 . . . . . . . . . . . . . . . . . . 19  |-  -.  <. n ,  x >.  =  (/)
55 eqeq1 2457 . . . . . . . . . . . . . . . . . . 19  |-  ( if ( x  e.  ( _V  X.  U ) ,  <. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. )  =  <. n ,  x >.  ->  ( if ( x  e.  ( _V  X.  U ) ,  <. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. )  =  (/)  <->  <. n ,  x >.  =  (/) ) )
5654, 55mtbiri 305 . . . . . . . . . . . . . . . . . 18  |-  ( if ( x  e.  ( _V  X.  U ) ,  <. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. )  =  <. n ,  x >.  ->  -.  if ( x  e.  ( _V  X.  U ) ,  <. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. )  =  (/) )
5751, 56jaoi 381 . . . . . . . . . . . . . . . . 17  |-  ( ( if ( x  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  x
) >. ,  <. n ,  x >. )  =  <. U. n ,  ( 1st `  x ) >.  \/  if ( x  e.  ( _V  X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. )  =  <. n ,  x >. )  ->  -.  if ( x  e.  ( _V  X.  U ) ,  <. U. n ,  ( 1st `  x ) >. ,  <. n ,  x >. )  =  (/) )
5844, 57mp1i 13 . . . . . . . . . . . . . . . 16  |-  ( ( -.  X  e.  U  /\  x  =  X
)  ->  -.  if ( x  e.  ( _V  X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. )  =  (/) )
5958neqned 2633 . . . . . . . . . . . . . . 15  |-  ( ( -.  X  e.  U  /\  x  =  X
)  ->  if (
x  e.  ( _V 
X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. )  =/=  (/) )
6043, 59eqnetrd 2693 . . . . . . . . . . . . . 14  |-  ( ( -.  X  e.  U  /\  x  =  X
)  ->  if (
( n  =  1o 
/\  x  e.  U
) ,  (/) ,  if ( x  e.  ( _V  X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. ) )  =/=  (/) )
6160adantrl 723 . . . . . . . . . . . . 13  |-  ( ( -.  X  e.  U  /\  ( n  =  1o 
/\  x  =  X ) )  ->  if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  x
) >. ,  <. n ,  x >. ) )  =/=  (/) )
6234, 61eqnetrrd 2694 . . . . . . . . . . . 12  |-  ( ( -.  X  e.  U  /\  ( n  =  1o 
/\  x  =  X ) )  ->  [_ 1o  /  n ]_ [_ X  /  x ]_ if ( ( n  =  1o 
/\  x  e.  U
) ,  (/) ,  if ( x  e.  ( _V  X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. ) )  =/=  (/) )
6362adantl 468 . . . . . . . . . . 11  |-  ( ( X  e.  _V  /\  ( -.  X  e.  U  /\  ( n  =  1o  /\  x  =  X ) ) )  ->  [_ 1o  /  n ]_ [_ X  /  x ]_ if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  x
) >. ,  <. n ,  x >. ) )  =/=  (/) )
6430, 63eqnetrd 2693 . . . . . . . . . 10  |-  ( ( X  e.  _V  /\  ( -.  X  e.  U  /\  ( n  =  1o  /\  x  =  X ) ) )  ->  ( 1o ( n  e.  om ,  x  e.  _V  |->  if ( ( n  =  1o 
/\  x  e.  U
) ,  (/) ,  if ( x  e.  ( _V  X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. ) ) ) X )  =/=  (/) )
6519, 64syl5eqner 2701 . . . . . . . . 9  |-  ( ( X  e.  _V  /\  ( -.  X  e.  U  /\  ( n  =  1o  /\  x  =  X ) ) )  ->  ( ( n  e.  om ,  x  e.  _V  |->  if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V 
X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. ) ) ) `
 <. 1o ,  X >. )  =/=  (/) )
6665ancom2s 812 . . . . . . . 8  |-  ( ( X  e.  _V  /\  ( ( n  =  1o  /\  x  =  X )  /\  -.  X  e.  U )
)  ->  ( (
n  e.  om ,  x  e.  _V  |->  if ( ( n  =  1o 
/\  x  e.  U
) ,  (/) ,  if ( x  e.  ( _V  X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. ) ) ) `
 <. 1o ,  X >. )  =/=  (/) )
6766an12s 811 . . . . . . 7  |-  ( ( ( n  =  1o 
/\  x  =  X )  /\  ( X  e.  _V  /\  -.  X  e.  U )
)  ->  ( (
n  e.  om ,  x  e.  _V  |->  if ( ( n  =  1o 
/\  x  e.  U
) ,  (/) ,  if ( x  e.  ( _V  X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. ) ) ) `
 <. 1o ,  X >. )  =/=  (/) )
6867exp31 609 . . . . . 6  |-  ( n  =  1o  ->  (
x  =  X  -> 
( ( X  e. 
_V  /\  -.  X  e.  U )  ->  (
( n  e.  om ,  x  e.  _V  |->  if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  x
) >. ,  <. n ,  x >. ) ) ) `
 <. 1o ,  X >. )  =/=  (/) ) ) )
6916, 18, 68vtoclef 3124 . . . . 5  |-  ( x  =  X  ->  (
( X  e.  _V  /\ 
-.  X  e.  U
)  ->  ( (
n  e.  om ,  x  e.  _V  |->  if ( ( n  =  1o 
/\  x  e.  U
) ,  (/) ,  if ( x  e.  ( _V  X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. ) ) ) `
 <. 1o ,  X >. )  =/=  (/) ) )
707, 69vtoclefex 31748 . . . 4  |-  ( X  e.  _V  ->  (
( X  e.  _V  /\ 
-.  X  e.  U
)  ->  ( (
n  e.  om ,  x  e.  _V  |->  if ( ( n  =  1o 
/\  x  e.  U
) ,  (/) ,  if ( x  e.  ( _V  X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. ) ) ) `
 <. 1o ,  X >. )  =/=  (/) ) )
7170anabsi5 827 . . 3  |-  ( ( X  e.  _V  /\  -.  X  e.  U
)  ->  ( (
n  e.  om ,  x  e.  _V  |->  if ( ( n  =  1o 
/\  x  e.  U
) ,  (/) ,  if ( x  e.  ( _V  X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. ) ) ) `
 <. 1o ,  X >. )  =/=  (/) )
7271necomd 2681 . 2  |-  ( ( X  e.  _V  /\  -.  X  e.  U
)  ->  (/)  =/=  (
( n  e.  om ,  x  e.  _V  |->  if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  x
) >. ,  <. n ,  x >. ) ) ) `
 <. 1o ,  X >. ) )
7372neneqd 2631 1  |-  ( ( X  e.  _V  /\  -.  X  e.  U
)  ->  -.  (/)  =  ( ( n  e.  om ,  x  e.  _V  |->  if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  x
) >. ,  <. n ,  x >. ) ) ) `
 <. 1o ,  X >. ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 370    /\ wa 371    = wceq 1446    e. wcel 1889    =/= wne 2624   _Vcvv 3047   [_csb 3365   (/)c0 3733   ifcif 3883   <.cop 3976   U.cuni 4201    X. cxp 4835   ` cfv 5585  (class class class)co 6295    |-> cmpt2 6297   omcom 6697   1stc1st 6796   1oc1o 7180
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pr 4642  ax-un 6588
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 987  df-3an 988  df-tru 1449  df-fal 1452  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-rab 2748  df-v 3049  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-tp 3975  df-op 3977  df-uni 4202  df-br 4406  df-opab 4465  df-tr 4501  df-eprel 4748  df-id 4752  df-po 4758  df-so 4759  df-fr 4796  df-we 4798  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-ord 5429  df-on 5430  df-lim 5431  df-suc 5432  df-iota 5549  df-fun 5587  df-fv 5593  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-om 6698  df-1o 7187
This theorem is referenced by:  finxp1o  31796
  Copyright terms: Public domain W3C validator