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

Theorem nninfdclemf1 12506
Description: Lemma for nninfdc 12507. The function from nninfdclemf 12503 is one-to-one. (Contributed by Jim Kingdon, 23-Sep-2024.)
Hypotheses
Ref Expression
nninfdclemf.a  |-  ( ph  ->  A  C_  NN )
nninfdclemf.dc  |-  ( ph  ->  A. x  e.  NN DECID  x  e.  A )
nninfdclemf.nb  |-  ( ph  ->  A. m  e.  NN  E. n  e.  A  m  <  n )
nninfdclemf.j  |-  ( ph  ->  ( J  e.  A  /\  1  <  J ) )
nninfdclemf.f  |-  F  =  seq 1 ( ( y  e.  NN , 
z  e.  NN  |-> inf ( ( A  i^i  ( ZZ>=
`  ( y  +  1 ) ) ) ,  RR ,  <  ) ) ,  ( i  e.  NN  |->  J ) )
Assertion
Ref Expression
nninfdclemf1  |-  ( ph  ->  F : NN -1-1-> A
)
Distinct variable groups:    A, m, n   
x, A    y, A, z    m, F, n    x, F    y, F, z    i, J    y, J, z
Allowed substitution hints:    ph( x, y, z, i, m, n)    A( i)    F( i)    J( x, m, n)

Proof of Theorem nninfdclemf1
Dummy variables  p  q  u  v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nninfdclemf.a . . 3  |-  ( ph  ->  A  C_  NN )
2 nninfdclemf.dc . . 3  |-  ( ph  ->  A. x  e.  NN DECID  x  e.  A )
3 nninfdclemf.nb . . 3  |-  ( ph  ->  A. m  e.  NN  E. n  e.  A  m  <  n )
4 nninfdclemf.j . . 3  |-  ( ph  ->  ( J  e.  A  /\  1  <  J ) )
5 nninfdclemf.f . . 3  |-  F  =  seq 1 ( ( y  e.  NN , 
z  e.  NN  |-> inf ( ( A  i^i  ( ZZ>=
`  ( y  +  1 ) ) ) ,  RR ,  <  ) ) ,  ( i  e.  NN  |->  J ) )
61, 2, 3, 4, 5nninfdclemf 12503 . 2  |-  ( ph  ->  F : NN --> A )
7 fveq2 5534 . . . . 5  |-  ( u  =  v  ->  ( F `  u )  =  ( F `  v ) )
8 fveq2 5534 . . . . 5  |-  ( u  =  p  ->  ( F `  u )  =  ( F `  p ) )
9 fveq2 5534 . . . . 5  |-  ( u  =  q  ->  ( F `  u )  =  ( F `  q ) )
10 nnssre 8954 . . . . 5  |-  NN  C_  RR
111adantr 276 . . . . . . 7  |-  ( (
ph  /\  u  e.  NN )  ->  A  C_  NN )
126ffvelcdmda 5672 . . . . . . 7  |-  ( (
ph  /\  u  e.  NN )  ->  ( F `
 u )  e.  A )
1311, 12sseldd 3171 . . . . . 6  |-  ( (
ph  /\  u  e.  NN )  ->  ( F `
 u )  e.  NN )
1413nnred 8963 . . . . 5  |-  ( (
ph  /\  u  e.  NN )  ->  ( F `
 u )  e.  RR )
151ad2antrr 488 . . . . . . 7  |-  ( ( ( ph  /\  (
u  e.  NN  /\  v  e.  NN )
)  /\  u  <  v )  ->  A  C_  NN )
162ad2antrr 488 . . . . . . 7  |-  ( ( ( ph  /\  (
u  e.  NN  /\  v  e.  NN )
)  /\  u  <  v )  ->  A. x  e.  NN DECID  x  e.  A )
173ad2antrr 488 . . . . . . 7  |-  ( ( ( ph  /\  (
u  e.  NN  /\  v  e.  NN )
)  /\  u  <  v )  ->  A. m  e.  NN  E. n  e.  A  m  <  n
)
184ad2antrr 488 . . . . . . 7  |-  ( ( ( ph  /\  (
u  e.  NN  /\  v  e.  NN )
)  /\  u  <  v )  ->  ( J  e.  A  /\  1  <  J ) )
19 simplrl 535 . . . . . . 7  |-  ( ( ( ph  /\  (
u  e.  NN  /\  v  e.  NN )
)  /\  u  <  v )  ->  u  e.  NN )
20 simplrr 536 . . . . . . 7  |-  ( ( ( ph  /\  (
u  e.  NN  /\  v  e.  NN )
)  /\  u  <  v )  ->  v  e.  NN )
21 simpr 110 . . . . . . 7  |-  ( ( ( ph  /\  (
u  e.  NN  /\  v  e.  NN )
)  /\  u  <  v )  ->  u  <  v )
2215, 16, 17, 18, 5, 19, 20, 21nninfdclemlt 12505 . . . . . 6  |-  ( ( ( ph  /\  (
u  e.  NN  /\  v  e.  NN )
)  /\  u  <  v )  ->  ( F `  u )  <  ( F `  v )
)
2322ex 115 . . . . 5  |-  ( (
ph  /\  ( u  e.  NN  /\  v  e.  NN ) )  -> 
( u  <  v  ->  ( F `  u
)  <  ( F `  v ) ) )
247, 8, 9, 10, 14, 23eqord1 8471 . . . 4  |-  ( (
ph  /\  ( p  e.  NN  /\  q  e.  NN ) )  -> 
( p  =  q  <-> 
( F `  p
)  =  ( F `
 q ) ) )
2524biimprd 158 . . 3  |-  ( (
ph  /\  ( p  e.  NN  /\  q  e.  NN ) )  -> 
( ( F `  p )  =  ( F `  q )  ->  p  =  q ) )
2625ralrimivva 2572 . 2  |-  ( ph  ->  A. p  e.  NN  A. q  e.  NN  (
( F `  p
)  =  ( F `
 q )  ->  p  =  q )
)
27 dff13 5790 . 2  |-  ( F : NN -1-1-> A  <->  ( F : NN --> A  /\  A. p  e.  NN  A. q  e.  NN  ( ( F `
 p )  =  ( F `  q
)  ->  p  =  q ) ) )
286, 26, 27sylanbrc 417 1  |-  ( ph  ->  F : NN -1-1-> A
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104  DECID wdc 835    = wceq 1364    e. wcel 2160   A.wral 2468   E.wrex 2469    i^i cin 3143    C_ wss 3144   class class class wbr 4018    |-> cmpt 4079   -->wf 5231   -1-1->wf1 5232   ` cfv 5235  (class class class)co 5897    e. cmpo 5899  infcinf 7013   RRcr 7841   1c1 7843    + caddc 7845    < clt 8023   NNcn 8950   ZZ>=cuz 9559    seqcseq 10478
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 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4133  ax-sep 4136  ax-nul 4144  ax-pow 4192  ax-pr 4227  ax-un 4451  ax-setind 4554  ax-iinf 4605  ax-cnex 7933  ax-resscn 7934  ax-1cn 7935  ax-1re 7936  ax-icn 7937  ax-addcl 7938  ax-addrcl 7939  ax-mulcl 7940  ax-addcom 7942  ax-addass 7944  ax-distr 7946  ax-i2m1 7947  ax-0lt1 7948  ax-0id 7950  ax-rnegex 7951  ax-cnre 7953  ax-pre-ltirr 7954  ax-pre-ltwlin 7955  ax-pre-lttrn 7956  ax-pre-apti 7957  ax-pre-ltadd 7958
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-nel 2456  df-ral 2473  df-rex 2474  df-reu 2475  df-rmo 2476  df-rab 2477  df-v 2754  df-sbc 2978  df-csb 3073  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-nul 3438  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-iun 3903  df-br 4019  df-opab 4080  df-mpt 4081  df-tr 4117  df-id 4311  df-po 4314  df-iso 4315  df-iord 4384  df-on 4386  df-ilim 4387  df-suc 4389  df-iom 4608  df-xp 4650  df-rel 4651  df-cnv 4652  df-co 4653  df-dm 4654  df-rn 4655  df-res 4656  df-ima 4657  df-iota 5196  df-fun 5237  df-fn 5238  df-f 5239  df-f1 5240  df-fo 5241  df-f1o 5242  df-fv 5243  df-isom 5244  df-riota 5852  df-ov 5900  df-oprab 5901  df-mpo 5902  df-1st 6166  df-2nd 6167  df-recs 6331  df-frec 6417  df-sup 7014  df-inf 7015  df-pnf 8025  df-mnf 8026  df-xr 8027  df-ltxr 8028  df-le 8029  df-sub 8161  df-neg 8162  df-inn 8951  df-n0 9208  df-z 9285  df-uz 9560  df-fz 10041  df-fzo 10175  df-seqfrec 10479
This theorem is referenced by:  nninfdc  12507
  Copyright terms: Public domain W3C validator