ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ennnfonelemj0 Unicode version

Theorem ennnfonelemj0 12404
Description: Lemma for ennnfone 12428. Initial state for  J. (Contributed by Jim Kingdon, 20-Jul-2023.)
Hypotheses
Ref Expression
ennnfonelemh.dceq  |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )
ennnfonelemh.f  |-  ( ph  ->  F : om -onto-> A
)
ennnfonelemh.ne  |-  ( ph  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `  k )  =/=  ( F `  j ) )
ennnfonelemh.g  |-  G  =  ( x  e.  ( A  ^pm  om ) ,  y  e.  om  |->  if ( ( F `  y )  e.  ( F " y ) ,  x ,  ( x  u.  { <. dom  x ,  ( F `
 y ) >. } ) ) )
ennnfonelemh.n  |-  N  = frec ( ( x  e.  ZZ  |->  ( x  + 
1 ) ) ,  0 )
ennnfonelemh.j  |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/) ,  ( `' N `  ( x  -  1 ) ) ) )
ennnfonelemh.h  |-  H  =  seq 0 ( G ,  J )
Assertion
Ref Expression
ennnfonelemj0  |-  ( ph  ->  ( J `  0
)  e.  { g  e.  ( A  ^pm  om )  |  dom  g  e.  om } )
Distinct variable groups:    A, g    x, N
Allowed substitution hints:    ph( x, y, g, j, k, n)    A( x, y, j, k, n)    F( x, y, g, j, k, n)    G( x, y, g, j, k, n)    H( x, y, g, j, k, n)    J( x, y, g, j, k, n)    N( y, g, j, k, n)

Proof of Theorem ennnfonelemj0
StepHypRef Expression
1 0nn0 9193 . . . 4  |-  0  e.  NN0
2 eqid 2177 . . . . . 6  |-  0  =  0
32iftruei 3542 . . . . 5  |-  if ( 0  =  0 ,  (/) ,  ( `' N `  ( 0  -  1 ) ) )  =  (/)
4 0ex 4132 . . . . 5  |-  (/)  e.  _V
53, 4eqeltri 2250 . . . 4  |-  if ( 0  =  0 ,  (/) ,  ( `' N `  ( 0  -  1 ) ) )  e. 
_V
6 eqeq1 2184 . . . . . 6  |-  ( x  =  0  ->  (
x  =  0  <->  0  =  0 ) )
7 fvoveq1 5900 . . . . . 6  |-  ( x  =  0  ->  ( `' N `  ( x  -  1 ) )  =  ( `' N `  ( 0  -  1 ) ) )
86, 7ifbieq2d 3560 . . . . 5  |-  ( x  =  0  ->  if ( x  =  0 ,  (/) ,  ( `' N `  ( x  -  1 ) ) )  =  if ( 0  =  0 ,  (/) ,  ( `' N `  ( 0  -  1 ) ) ) )
9 ennnfonelemh.j . . . . 5  |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/) ,  ( `' N `  ( x  -  1 ) ) ) )
108, 9fvmptg 5594 . . . 4  |-  ( ( 0  e.  NN0  /\  if ( 0  =  0 ,  (/) ,  ( `' N `  ( 0  -  1 ) ) )  e.  _V )  ->  ( J `  0
)  =  if ( 0  =  0 ,  (/) ,  ( `' N `  ( 0  -  1 ) ) ) )
111, 5, 10mp2an 426 . . 3  |-  ( J `
 0 )  =  if ( 0  =  0 ,  (/) ,  ( `' N `  ( 0  -  1 ) ) )
1211, 3eqtri 2198 . 2  |-  ( J `
 0 )  =  (/)
13 dmeq 4829 . . . 4  |-  ( g  =  (/)  ->  dom  g  =  dom  (/) )
1413eleq1d 2246 . . 3  |-  ( g  =  (/)  ->  ( dom  g  e.  om  <->  dom  (/)  e.  om ) )
15 fun0 5276 . . . . 5  |-  Fun  (/)
16 0ss 3463 . . . . 5  |-  (/)  C_  ( om  X.  A )
1715, 16pm3.2i 272 . . . 4  |-  ( Fun  (/)  /\  (/)  C_  ( om  X.  A ) )
18 omex 4594 . . . . . 6  |-  om  e.  _V
19 ennnfonelemh.f . . . . . 6  |-  ( ph  ->  F : om -onto-> A
)
20 focdmex 6118 . . . . . 6  |-  ( om  e.  _V  ->  ( F : om -onto-> A  ->  A  e.  _V )
)
2118, 19, 20mpsyl 65 . . . . 5  |-  ( ph  ->  A  e.  _V )
22 elpmg 6666 . . . . 5  |-  ( ( A  e.  _V  /\  om  e.  _V )  -> 
( (/)  e.  ( A 
^pm  om )  <->  ( Fun  (/) 
/\  (/)  C_  ( om  X.  A ) ) ) )
2321, 18, 22sylancl 413 . . . 4  |-  ( ph  ->  ( (/)  e.  ( A  ^pm  om )  <->  ( Fun  (/) 
/\  (/)  C_  ( om  X.  A ) ) ) )
2417, 23mpbiri 168 . . 3  |-  ( ph  -> 
(/)  e.  ( A  ^pm  om ) )
25 dm0 4843 . . . . 5  |-  dom  (/)  =  (/)
26 peano1 4595 . . . . 5  |-  (/)  e.  om
2725, 26eqeltri 2250 . . . 4  |-  dom  (/)  e.  om
2827a1i 9 . . 3  |-  ( ph  ->  dom  (/)  e.  om )
2914, 24, 28elrabd 2897 . 2  |-  ( ph  -> 
(/)  e.  { g  e.  ( A  ^pm  om )  |  dom  g  e.  om } )
3012, 29eqeltrid 2264 1  |-  ( ph  ->  ( J `  0
)  e.  { g  e.  ( A  ^pm  om )  |  dom  g  e.  om } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105  DECID wdc 834    = wceq 1353    e. wcel 2148    =/= wne 2347   A.wral 2455   E.wrex 2456   {crab 2459   _Vcvv 2739    u. cun 3129    C_ wss 3131   (/)c0 3424   ifcif 3536   {csn 3594   <.cop 3597    |-> cmpt 4066   suc csuc 4367   omcom 4591    X. cxp 4626   `'ccnv 4627   dom cdm 4628   "cima 4631   Fun wfun 5212   -onto->wfo 5216   ` cfv 5218  (class class class)co 5877    e. cmpo 5879  freccfrec 6393    ^pm cpm 6651   0cc0 7813   1c1 7814    + caddc 7816    - cmin 8130   NN0cn0 9178   ZZcz 9255    seqcseq 10447
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4120  ax-sep 4123  ax-nul 4131  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-iinf 4589  ax-1cn 7906  ax-icn 7908  ax-addcl 7909  ax-mulcl 7911  ax-i2m1 7918
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-if 3537  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-id 4295  df-iom 4592  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-ov 5880  df-oprab 5881  df-mpo 5882  df-pm 6653  df-n0 9179
This theorem is referenced by:  ennnfonelemh  12407  ennnfonelem0  12408  ennnfonelemp1  12409  ennnfonelemom  12411
  Copyright terms: Public domain W3C validator