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

Theorem finxpreclem3 31749
Description: Lemma for  ^^ ^^ recursion theorems. (Contributed by ML, 20-Oct-2020.)
Hypothesis
Ref Expression
finxpreclem3.1  |-  F  =  ( n  e.  om ,  x  e.  _V  |->  if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  x
) >. ,  <. n ,  x >. ) ) )
Assertion
Ref Expression
finxpreclem3  |-  ( ( ( N  e.  om  /\  2o  C_  N )  /\  X  e.  ( _V  X.  U ) )  ->  <. U. N ,  ( 1st `  X )
>.  =  ( F `  <. N ,  X >. ) )
Distinct variable groups:    n, N, x    U, n, x    n, X, x
Allowed substitution hints:    F( x, n)

Proof of Theorem finxpreclem3
StepHypRef Expression
1 df-ov 6308 . 2  |-  ( N F X )  =  ( F `  <. N ,  X >. )
2 finxpreclem3.1 . . . 4  |-  F  =  ( n  e.  om ,  x  e.  _V  |->  if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  x
) >. ,  <. n ,  x >. ) ) )
32a1i 11 . . 3  |-  ( ( ( N  e.  om  /\  2o  C_  N )  /\  X  e.  ( _V  X.  U ) )  ->  F  =  ( n  e.  om ,  x  e.  _V  |->  if ( ( n  =  1o 
/\  x  e.  U
) ,  (/) ,  if ( x  e.  ( _V  X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. ) ) ) )
4 eqeq1 2426 . . . . . . 7  |-  ( n  =  N  ->  (
n  =  1o  <->  N  =  1o ) )
5 eleq1 2495 . . . . . . 7  |-  ( x  =  X  ->  (
x  e.  U  <->  X  e.  U ) )
64, 5bi2anan9 881 . . . . . 6  |-  ( ( n  =  N  /\  x  =  X )  ->  ( ( n  =  1o  /\  x  e.  U )  <->  ( N  =  1o  /\  X  e.  U ) ) )
7 eleq1 2495 . . . . . . . 8  |-  ( x  =  X  ->  (
x  e.  ( _V 
X.  U )  <->  X  e.  ( _V  X.  U
) ) )
87adantl 467 . . . . . . 7  |-  ( ( n  =  N  /\  x  =  X )  ->  ( x  e.  ( _V  X.  U )  <-> 
X  e.  ( _V 
X.  U ) ) )
9 unieq 4227 . . . . . . . . 9  |-  ( n  =  N  ->  U. n  =  U. N )
109adantr 466 . . . . . . . 8  |-  ( ( n  =  N  /\  x  =  X )  ->  U. n  =  U. N )
11 fveq2 5881 . . . . . . . . 9  |-  ( x  =  X  ->  ( 1st `  x )  =  ( 1st `  X
) )
1211adantl 467 . . . . . . . 8  |-  ( ( n  =  N  /\  x  =  X )  ->  ( 1st `  x
)  =  ( 1st `  X ) )
1310, 12opeq12d 4195 . . . . . . 7  |-  ( ( n  =  N  /\  x  =  X )  -> 
<. U. n ,  ( 1st `  x )
>.  =  <. U. N ,  ( 1st `  X
) >. )
14 opeq12 4189 . . . . . . 7  |-  ( ( n  =  N  /\  x  =  X )  -> 
<. n ,  x >.  = 
<. N ,  X >. )
158, 13, 14ifbieq12d 3938 . . . . . 6  |-  ( ( n  =  N  /\  x  =  X )  ->  if ( x  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  x
) >. ,  <. n ,  x >. )  =  if ( X  e.  ( _V  X.  U ) ,  <. U. N ,  ( 1st `  X )
>. ,  <. N ,  X >. ) )
166, 15ifbieq2d 3936 . . . . 5  |-  ( ( n  =  N  /\  x  =  X )  ->  if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  x
) >. ,  <. n ,  x >. ) )  =  if ( ( N  =  1o  /\  X  e.  U ) ,  (/) ,  if ( X  e.  ( _V  X.  U
) ,  <. U. N ,  ( 1st `  X
) >. ,  <. N ,  X >. ) ) )
17 sssucid 5519 . . . . . . . . . . . . 13  |-  1o  C_  suc  1o
18 df-2o 7194 . . . . . . . . . . . . 13  |-  2o  =  suc  1o
1917, 18sseqtr4i 3497 . . . . . . . . . . . 12  |-  1o  C_  2o
20 1on 7200 . . . . . . . . . . . . . 14  |-  1o  e.  On
2118, 20sucneqoni 31733 . . . . . . . . . . . . 13  |-  2o  =/=  1o
2221necomi 2690 . . . . . . . . . . . 12  |-  1o  =/=  2o
23 df-pss 3452 . . . . . . . . . . . 12  |-  ( 1o  C.  2o  <->  ( 1o  C_  2o  /\  1o  =/=  2o ) )
2419, 22, 23mpbir2an 928 . . . . . . . . . . 11  |-  1o  C.  2o
25 ssnpss 3568 . . . . . . . . . . 11  |-  ( 2o  C_  1o  ->  -.  1o  C.  2o )
2624, 25mt2 182 . . . . . . . . . 10  |-  -.  2o  C_  1o
27 sseq2 3486 . . . . . . . . . 10  |-  ( N  =  1o  ->  ( 2o  C_  N  <->  2o  C_  1o ) )
2826, 27mtbiri 304 . . . . . . . . 9  |-  ( N  =  1o  ->  -.  2o  C_  N )
2928con2i 123 . . . . . . . 8  |-  ( 2o  C_  N  ->  -.  N  =  1o )
3029intnanrd 925 . . . . . . 7  |-  ( 2o  C_  N  ->  -.  ( N  =  1o  /\  X  e.  U ) )
3130iffalsed 3922 . . . . . 6  |-  ( 2o  C_  N  ->  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 >. ) )
32 iftrue 3917 . . . . . 6  |-  ( X  e.  ( _V  X.  U )  ->  if ( X  e.  ( _V  X.  U ) , 
<. U. N ,  ( 1st `  X )
>. ,  <. N ,  X >. )  =  <. U. N ,  ( 1st `  X ) >. )
3331, 32sylan9eq 2483 . . . . 5  |-  ( ( 2o  C_  N  /\  X  e.  ( _V  X.  U ) )  ->  if ( ( N  =  1o  /\  X  e.  U ) ,  (/) ,  if ( X  e.  ( _V  X.  U
) ,  <. U. N ,  ( 1st `  X
) >. ,  <. N ,  X >. ) )  = 
<. U. N ,  ( 1st `  X )
>. )
3416, 33sylan9eqr 2485 . . . 4  |-  ( ( ( 2o  C_  N  /\  X  e.  ( _V  X.  U ) )  /\  ( n  =  N  /\  x  =  X ) )  ->  if ( ( n  =  1o  /\  x  e.  U ) ,  (/) ,  if ( x  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  x
) >. ,  <. n ,  x >. ) )  = 
<. U. N ,  ( 1st `  X )
>. )
3534adantlll 722 . . 3  |-  ( ( ( ( N  e. 
om  /\  2o  C_  N
)  /\  X  e.  ( _V  X.  U
) )  /\  (
n  =  N  /\  x  =  X )
)  ->  if (
( n  =  1o 
/\  x  e.  U
) ,  (/) ,  if ( x  e.  ( _V  X.  U ) , 
<. U. n ,  ( 1st `  x )
>. ,  <. n ,  x >. ) )  = 
<. U. N ,  ( 1st `  X )
>. )
36 simpll 758 . . 3  |-  ( ( ( N  e.  om  /\  2o  C_  N )  /\  X  e.  ( _V  X.  U ) )  ->  N  e.  om )
37 elex 3089 . . . 4  |-  ( X  e.  ( _V  X.  U )  ->  X  e.  _V )
3837adantl 467 . . 3  |-  ( ( ( N  e.  om  /\  2o  C_  N )  /\  X  e.  ( _V  X.  U ) )  ->  X  e.  _V )
39 opex 4685 . . . 4  |-  <. U. N ,  ( 1st `  X
) >.  e.  _V
4039a1i 11 . . 3  |-  ( ( ( N  e.  om  /\  2o  C_  N )  /\  X  e.  ( _V  X.  U ) )  ->  <. U. N ,  ( 1st `  X )
>.  e.  _V )
413, 35, 36, 38, 40ovmpt2d 6438 . 2  |-  ( ( ( N  e.  om  /\  2o  C_  N )  /\  X  e.  ( _V  X.  U ) )  ->  ( N F X )  =  <. U. N ,  ( 1st `  X ) >. )
421, 41syl5reqr 2478 1  |-  ( ( ( N  e.  om  /\  2o  C_  N )  /\  X  e.  ( _V  X.  U ) )  ->  <. U. N ,  ( 1st `  X )
>.  =  ( F `  <. N ,  X >. ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437    e. wcel 1872    =/= wne 2614   _Vcvv 3080    C_ wss 3436    C. wpss 3437   (/)c0 3761   ifcif 3911   <.cop 4004   U.cuni 4219    X. cxp 4851   suc csuc 5444   ` cfv 5601  (class class class)co 6305    |-> cmpt2 6307   omcom 6706   1stc1st 6805   1oc1o 7186   2oc2o 7187
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660  ax-un 6597
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-ord 5445  df-on 5446  df-suc 5448  df-iota 5565  df-fun 5603  df-fv 5609  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-1o 7193  df-2o 7194
This theorem is referenced by:  finxpreclem4  31750
  Copyright terms: Public domain W3C validator