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

Theorem frec2uzf1od 9166
Description: 𝐺 (see frec2uz0d 9159) is a one-to-one onto mapping. (Contributed by Jim Kingdon, 17-May-2020.)
Hypotheses
Ref Expression
frec2uz.1 (𝜑𝐶 ∈ ℤ)
frec2uz.2 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 𝐶)
Assertion
Ref Expression
frec2uzf1od (𝜑𝐺:ω–1-1-onto→(ℤ𝐶))
Distinct variable groups:   𝑥,𝐶   𝜑,𝑥
Allowed substitution hint:   𝐺(𝑥)

Proof of Theorem frec2uzf1od
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 zex 8252 . . . . . . . . 9 ℤ ∈ V
21mptex 5387 . . . . . . . 8 (𝑥 ∈ ℤ ↦ (𝑥 + 1)) ∈ V
3 vex 2560 . . . . . . . 8 𝑧 ∈ V
42, 3fvex 5195 . . . . . . 7 ((𝑥 ∈ ℤ ↦ (𝑥 + 1))‘𝑧) ∈ V
54ax-gen 1338 . . . . . 6 𝑧((𝑥 ∈ ℤ ↦ (𝑥 + 1))‘𝑧) ∈ V
6 frec2uz.1 . . . . . 6 (𝜑𝐶 ∈ ℤ)
7 frecfnom 5986 . . . . . 6 ((∀𝑧((𝑥 ∈ ℤ ↦ (𝑥 + 1))‘𝑧) ∈ V ∧ 𝐶 ∈ ℤ) → frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 𝐶) Fn ω)
85, 6, 7sylancr 393 . . . . 5 (𝜑 → frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 𝐶) Fn ω)
9 frec2uz.2 . . . . . 6 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 𝐶)
109fneq1i 4993 . . . . 5 (𝐺 Fn ω ↔ frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 𝐶) Fn ω)
118, 10sylibr 137 . . . 4 (𝜑𝐺 Fn ω)
126, 9frec2uzrand 9165 . . . . 5 (𝜑 → ran 𝐺 = (ℤ𝐶))
13 eqimss 2997 . . . . 5 (ran 𝐺 = (ℤ𝐶) → ran 𝐺 ⊆ (ℤ𝐶))
1412, 13syl 14 . . . 4 (𝜑 → ran 𝐺 ⊆ (ℤ𝐶))
15 df-f 4906 . . . 4 (𝐺:ω⟶(ℤ𝐶) ↔ (𝐺 Fn ω ∧ ran 𝐺 ⊆ (ℤ𝐶)))
1611, 14, 15sylanbrc 394 . . 3 (𝜑𝐺:ω⟶(ℤ𝐶))
176adantr 261 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ω) → 𝐶 ∈ ℤ)
18 simpr 103 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ω) → 𝑦 ∈ ω)
1917, 9, 18frec2uzzd 9160 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ω) → (𝐺𝑦) ∈ ℤ)
20193adant3 924 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ω ∧ 𝑧 ∈ ω) → (𝐺𝑦) ∈ ℤ)
2120zred 8358 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ω ∧ 𝑧 ∈ ω) → (𝐺𝑦) ∈ ℝ)
2221ltnrd 7127 . . . . . . . . . 10 ((𝜑𝑦 ∈ ω ∧ 𝑧 ∈ ω) → ¬ (𝐺𝑦) < (𝐺𝑦))
2322adantr 261 . . . . . . . . 9 (((𝜑𝑦 ∈ ω ∧ 𝑧 ∈ ω) ∧ (𝐺𝑦) = (𝐺𝑧)) → ¬ (𝐺𝑦) < (𝐺𝑦))
24 simpr 103 . . . . . . . . . 10 (((𝜑𝑦 ∈ ω ∧ 𝑧 ∈ ω) ∧ (𝐺𝑦) = (𝐺𝑧)) → (𝐺𝑦) = (𝐺𝑧))
2524breq2d 3776 . . . . . . . . 9 (((𝜑𝑦 ∈ ω ∧ 𝑧 ∈ ω) ∧ (𝐺𝑦) = (𝐺𝑧)) → ((𝐺𝑦) < (𝐺𝑦) ↔ (𝐺𝑦) < (𝐺𝑧)))
2623, 25mtbid 597 . . . . . . . 8 (((𝜑𝑦 ∈ ω ∧ 𝑧 ∈ ω) ∧ (𝐺𝑦) = (𝐺𝑧)) → ¬ (𝐺𝑦) < (𝐺𝑧))
27173adant3 924 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ω ∧ 𝑧 ∈ ω) → 𝐶 ∈ ℤ)
28 simp2 905 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ω ∧ 𝑧 ∈ ω) → 𝑦 ∈ ω)
29 simp3 906 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ω ∧ 𝑧 ∈ ω) → 𝑧 ∈ ω)
3027, 9, 28, 29frec2uzltd 9163 . . . . . . . . . 10 ((𝜑𝑦 ∈ ω ∧ 𝑧 ∈ ω) → (𝑦𝑧 → (𝐺𝑦) < (𝐺𝑧)))
3130con3d 561 . . . . . . . . 9 ((𝜑𝑦 ∈ ω ∧ 𝑧 ∈ ω) → (¬ (𝐺𝑦) < (𝐺𝑧) → ¬ 𝑦𝑧))
3231adantr 261 . . . . . . . 8 (((𝜑𝑦 ∈ ω ∧ 𝑧 ∈ ω) ∧ (𝐺𝑦) = (𝐺𝑧)) → (¬ (𝐺𝑦) < (𝐺𝑧) → ¬ 𝑦𝑧))
3326, 32mpd 13 . . . . . . 7 (((𝜑𝑦 ∈ ω ∧ 𝑧 ∈ ω) ∧ (𝐺𝑦) = (𝐺𝑧)) → ¬ 𝑦𝑧)
3424breq1d 3774 . . . . . . . . 9 (((𝜑𝑦 ∈ ω ∧ 𝑧 ∈ ω) ∧ (𝐺𝑦) = (𝐺𝑧)) → ((𝐺𝑦) < (𝐺𝑦) ↔ (𝐺𝑧) < (𝐺𝑦)))
3523, 34mtbid 597 . . . . . . . 8 (((𝜑𝑦 ∈ ω ∧ 𝑧 ∈ ω) ∧ (𝐺𝑦) = (𝐺𝑧)) → ¬ (𝐺𝑧) < (𝐺𝑦))
3627, 9, 29, 28frec2uzltd 9163 . . . . . . . . 9 ((𝜑𝑦 ∈ ω ∧ 𝑧 ∈ ω) → (𝑧𝑦 → (𝐺𝑧) < (𝐺𝑦)))
3736adantr 261 . . . . . . . 8 (((𝜑𝑦 ∈ ω ∧ 𝑧 ∈ ω) ∧ (𝐺𝑦) = (𝐺𝑧)) → (𝑧𝑦 → (𝐺𝑧) < (𝐺𝑦)))
3835, 37mtod 589 . . . . . . 7 (((𝜑𝑦 ∈ ω ∧ 𝑧 ∈ ω) ∧ (𝐺𝑦) = (𝐺𝑧)) → ¬ 𝑧𝑦)
39 nntri3 6075 . . . . . . . . 9 ((𝑦 ∈ ω ∧ 𝑧 ∈ ω) → (𝑦 = 𝑧 ↔ (¬ 𝑦𝑧 ∧ ¬ 𝑧𝑦)))
40393adant1 922 . . . . . . . 8 ((𝜑𝑦 ∈ ω ∧ 𝑧 ∈ ω) → (𝑦 = 𝑧 ↔ (¬ 𝑦𝑧 ∧ ¬ 𝑧𝑦)))
4140adantr 261 . . . . . . 7 (((𝜑𝑦 ∈ ω ∧ 𝑧 ∈ ω) ∧ (𝐺𝑦) = (𝐺𝑧)) → (𝑦 = 𝑧 ↔ (¬ 𝑦𝑧 ∧ ¬ 𝑧𝑦)))
4233, 38, 41mpbir2and 851 . . . . . 6 (((𝜑𝑦 ∈ ω ∧ 𝑧 ∈ ω) ∧ (𝐺𝑦) = (𝐺𝑧)) → 𝑦 = 𝑧)
4342ex 108 . . . . 5 ((𝜑𝑦 ∈ ω ∧ 𝑧 ∈ ω) → ((𝐺𝑦) = (𝐺𝑧) → 𝑦 = 𝑧))
44433expb 1105 . . . 4 ((𝜑 ∧ (𝑦 ∈ ω ∧ 𝑧 ∈ ω)) → ((𝐺𝑦) = (𝐺𝑧) → 𝑦 = 𝑧))
4544ralrimivva 2401 . . 3 (𝜑 → ∀𝑦 ∈ ω ∀𝑧 ∈ ω ((𝐺𝑦) = (𝐺𝑧) → 𝑦 = 𝑧))
46 dff13 5407 . . 3 (𝐺:ω–1-1→(ℤ𝐶) ↔ (𝐺:ω⟶(ℤ𝐶) ∧ ∀𝑦 ∈ ω ∀𝑧 ∈ ω ((𝐺𝑦) = (𝐺𝑧) → 𝑦 = 𝑧)))
4716, 45, 46sylanbrc 394 . 2 (𝜑𝐺:ω–1-1→(ℤ𝐶))
48 dff1o5 5135 . 2 (𝐺:ω–1-1-onto→(ℤ𝐶) ↔ (𝐺:ω–1-1→(ℤ𝐶) ∧ ran 𝐺 = (ℤ𝐶)))
4947, 12, 48sylanbrc 394 1 (𝜑𝐺:ω–1-1-onto→(ℤ𝐶))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 97  wb 98  w3a 885  wal 1241   = wceq 1243  wcel 1393  wral 2306  Vcvv 2557  wss 2917   class class class wbr 3764  cmpt 3818  ωcom 4313  ran crn 4346   Fn wfn 4897  wf 4898  1-1wf1 4899  1-1-ontowf1o 4901  cfv 4902  (class class class)co 5512  freccfrec 5977  1c1 6888   + caddc 6890   < clt 7058  cz 8243  cuz 8471
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-13 1404  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-coll 3872  ax-sep 3875  ax-nul 3883  ax-pow 3927  ax-pr 3944  ax-un 4170  ax-setind 4262  ax-iinf 4311  ax-cnex 6973  ax-resscn 6974  ax-1cn 6975  ax-1re 6976  ax-icn 6977  ax-addcl 6978  ax-addrcl 6979  ax-mulcl 6980  ax-addcom 6982  ax-addass 6984  ax-distr 6986  ax-i2m1 6987  ax-0id 6990  ax-rnegex 6991  ax-cnre 6993  ax-pre-ltirr 6994  ax-pre-ltwlin 6995  ax-pre-lttrn 6996  ax-pre-ltadd 6998
This theorem depends on definitions:  df-bi 110  df-dc 743  df-3or 886  df-3an 887  df-tru 1246  df-fal 1249  df-nf 1350  df-sb 1646  df-eu 1903  df-mo 1904  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ne 2206  df-nel 2207  df-ral 2311  df-rex 2312  df-reu 2313  df-rab 2315  df-v 2559  df-sbc 2765  df-csb 2853  df-dif 2920  df-un 2922  df-in 2924  df-ss 2931  df-nul 3225  df-pw 3361  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-int 3616  df-iun 3659  df-br 3765  df-opab 3819  df-mpt 3820  df-tr 3855  df-eprel 4026  df-id 4030  df-po 4033  df-iso 4034  df-iord 4103  df-on 4105  df-suc 4108  df-iom 4314  df-xp 4351  df-rel 4352  df-cnv 4353  df-co 4354  df-dm 4355  df-rn 4356  df-res 4357  df-ima 4358  df-iota 4867  df-fun 4904  df-fn 4905  df-f 4906  df-f1 4907  df-fo 4908  df-f1o 4909  df-fv 4910  df-riota 5468  df-ov 5515  df-oprab 5516  df-mpt2 5517  df-1st 5767  df-2nd 5768  df-recs 5920  df-irdg 5957  df-frec 5978  df-1o 6001  df-2o 6002  df-oadd 6005  df-omul 6006  df-er 6106  df-ec 6108  df-qs 6112  df-ni 6400  df-pli 6401  df-mi 6402  df-lti 6403  df-plpq 6440  df-mpq 6441  df-enq 6443  df-nqqs 6444  df-plqqs 6445  df-mqqs 6446  df-1nqqs 6447  df-rq 6448  df-ltnqqs 6449  df-enq0 6520  df-nq0 6521  df-0nq0 6522  df-plq0 6523  df-mq0 6524  df-inp 6562  df-i1p 6563  df-iplp 6564  df-iltp 6566  df-enr 6809  df-nr 6810  df-ltr 6813  df-0r 6814  df-1r 6815  df-0 6894  df-1 6895  df-r 6897  df-lt 6900  df-pnf 7060  df-mnf 7061  df-xr 7062  df-ltxr 7063  df-le 7064  df-sub 7182  df-neg 7183  df-inn 7913  df-n0 8180  df-z 8244  df-uz 8472
This theorem is referenced by:  frec2uzisod  9167  frecuzrdglem  9171  frecuzrdgfn  9172  frecuzrdgcl  9173  frecuzrdgsuc  9175  uzenom  9176  frecfzennn  9177  frechashgf1o  9179
  Copyright terms: Public domain W3C validator