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

Theorem frecfzennn 10456
Description: The cardinality of a finite set of sequential integers. (See frec2uz0d 10429 for a description of the hypothesis.) (Contributed by Jim Kingdon, 18-May-2020.)
Hypothesis
Ref Expression
frecfzennn.1 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
Assertion
Ref Expression
frecfzennn (𝑁 ∈ ℕ0 → (1...𝑁) ≈ (𝐺𝑁))

Proof of Theorem frecfzennn
Dummy variables 𝑚 𝑛 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 5903 . . 3 (𝑛 = 0 → (1...𝑛) = (1...0))
2 fveq2 5534 . . 3 (𝑛 = 0 → (𝐺𝑛) = (𝐺‘0))
31, 2breq12d 4031 . 2 (𝑛 = 0 → ((1...𝑛) ≈ (𝐺𝑛) ↔ (1...0) ≈ (𝐺‘0)))
4 oveq2 5903 . . 3 (𝑛 = 𝑚 → (1...𝑛) = (1...𝑚))
5 fveq2 5534 . . 3 (𝑛 = 𝑚 → (𝐺𝑛) = (𝐺𝑚))
64, 5breq12d 4031 . 2 (𝑛 = 𝑚 → ((1...𝑛) ≈ (𝐺𝑛) ↔ (1...𝑚) ≈ (𝐺𝑚)))
7 oveq2 5903 . . 3 (𝑛 = (𝑚 + 1) → (1...𝑛) = (1...(𝑚 + 1)))
8 fveq2 5534 . . 3 (𝑛 = (𝑚 + 1) → (𝐺𝑛) = (𝐺‘(𝑚 + 1)))
97, 8breq12d 4031 . 2 (𝑛 = (𝑚 + 1) → ((1...𝑛) ≈ (𝐺𝑛) ↔ (1...(𝑚 + 1)) ≈ (𝐺‘(𝑚 + 1))))
10 oveq2 5903 . . 3 (𝑛 = 𝑁 → (1...𝑛) = (1...𝑁))
11 fveq2 5534 . . 3 (𝑛 = 𝑁 → (𝐺𝑛) = (𝐺𝑁))
1210, 11breq12d 4031 . 2 (𝑛 = 𝑁 → ((1...𝑛) ≈ (𝐺𝑛) ↔ (1...𝑁) ≈ (𝐺𝑁)))
13 0ex 4145 . . . 4 ∅ ∈ V
1413enref 6790 . . 3 ∅ ≈ ∅
15 fz10 10075 . . 3 (1...0) = ∅
16 0zd 9294 . . . . . . 7 (⊤ → 0 ∈ ℤ)
17 frecfzennn.1 . . . . . . 7 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
1816, 17frec2uzf1od 10436 . . . . . 6 (⊤ → 𝐺:ω–1-1-onto→(ℤ‘0))
1918mptru 1373 . . . . 5 𝐺:ω–1-1-onto→(ℤ‘0)
20 peano1 4611 . . . . 5 ∅ ∈ ω
2119, 20pm3.2i 272 . . . 4 (𝐺:ω–1-1-onto→(ℤ‘0) ∧ ∅ ∈ ω)
2216, 17frec2uz0d 10429 . . . . 5 (⊤ → (𝐺‘∅) = 0)
2322mptru 1373 . . . 4 (𝐺‘∅) = 0
24 f1ocnvfv 5800 . . . 4 ((𝐺:ω–1-1-onto→(ℤ‘0) ∧ ∅ ∈ ω) → ((𝐺‘∅) = 0 → (𝐺‘0) = ∅))
2521, 23, 24mp2 16 . . 3 (𝐺‘0) = ∅
2614, 15, 253brtr4i 4048 . 2 (1...0) ≈ (𝐺‘0)
27 simpr 110 . . . . 5 ((𝑚 ∈ ℕ0 ∧ (1...𝑚) ≈ (𝐺𝑚)) → (1...𝑚) ≈ (𝐺𝑚))
28 peano2nn0 9245 . . . . . . 7 (𝑚 ∈ ℕ0 → (𝑚 + 1) ∈ ℕ0)
29 zex 9291 . . . . . . . . . . . . . . 15 ℤ ∈ V
3029mptex 5762 . . . . . . . . . . . . . 14 (𝑥 ∈ ℤ ↦ (𝑥 + 1)) ∈ V
31 vex 2755 . . . . . . . . . . . . . 14 𝑧 ∈ V
3230, 31fvex 5554 . . . . . . . . . . . . 13 ((𝑥 ∈ ℤ ↦ (𝑥 + 1))‘𝑧) ∈ V
3332ax-gen 1460 . . . . . . . . . . . 12 𝑧((𝑥 ∈ ℤ ↦ (𝑥 + 1))‘𝑧) ∈ V
34 0z 9293 . . . . . . . . . . . 12 0 ∈ ℤ
35 frecfnom 6425 . . . . . . . . . . . 12 ((∀𝑧((𝑥 ∈ ℤ ↦ (𝑥 + 1))‘𝑧) ∈ V ∧ 0 ∈ ℤ) → frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) Fn ω)
3633, 34, 35mp2an 426 . . . . . . . . . . 11 frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) Fn ω
3717fneq1i 5329 . . . . . . . . . . 11 (𝐺 Fn ω ↔ frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) Fn ω)
3836, 37mpbir 146 . . . . . . . . . 10 𝐺 Fn ω
39 omex 4610 . . . . . . . . . 10 ω ∈ V
40 fnex 5758 . . . . . . . . . 10 ((𝐺 Fn ω ∧ ω ∈ V) → 𝐺 ∈ V)
4138, 39, 40mp2an 426 . . . . . . . . 9 𝐺 ∈ V
4241cnvex 5185 . . . . . . . 8 𝐺 ∈ V
43 vex 2755 . . . . . . . 8 𝑚 ∈ V
4442, 43fvex 5554 . . . . . . 7 (𝐺𝑚) ∈ V
45 en2sn 6838 . . . . . . 7 (((𝑚 + 1) ∈ ℕ0 ∧ (𝐺𝑚) ∈ V) → {(𝑚 + 1)} ≈ {(𝐺𝑚)})
4628, 44, 45sylancl 413 . . . . . 6 (𝑚 ∈ ℕ0 → {(𝑚 + 1)} ≈ {(𝐺𝑚)})
4746adantr 276 . . . . 5 ((𝑚 ∈ ℕ0 ∧ (1...𝑚) ≈ (𝐺𝑚)) → {(𝑚 + 1)} ≈ {(𝐺𝑚)})
48 fzp1disj 10109 . . . . . 6 ((1...𝑚) ∩ {(𝑚 + 1)}) = ∅
4948a1i 9 . . . . 5 ((𝑚 ∈ ℕ0 ∧ (1...𝑚) ≈ (𝐺𝑚)) → ((1...𝑚) ∩ {(𝑚 + 1)}) = ∅)
50 f1ocnvdm 5802 . . . . . . . . . 10 ((𝐺:ω–1-1-onto→(ℤ‘0) ∧ 𝑚 ∈ (ℤ‘0)) → (𝐺𝑚) ∈ ω)
5119, 50mpan 424 . . . . . . . . 9 (𝑚 ∈ (ℤ‘0) → (𝐺𝑚) ∈ ω)
52 nn0uz 9591 . . . . . . . . 9 0 = (ℤ‘0)
5351, 52eleq2s 2284 . . . . . . . 8 (𝑚 ∈ ℕ0 → (𝐺𝑚) ∈ ω)
54 nnord 4629 . . . . . . . 8 ((𝐺𝑚) ∈ ω → Ord (𝐺𝑚))
55 ordirr 4559 . . . . . . . 8 (Ord (𝐺𝑚) → ¬ (𝐺𝑚) ∈ (𝐺𝑚))
5653, 54, 553syl 17 . . . . . . 7 (𝑚 ∈ ℕ0 → ¬ (𝐺𝑚) ∈ (𝐺𝑚))
5756adantr 276 . . . . . 6 ((𝑚 ∈ ℕ0 ∧ (1...𝑚) ≈ (𝐺𝑚)) → ¬ (𝐺𝑚) ∈ (𝐺𝑚))
58 disjsn 3669 . . . . . 6 (((𝐺𝑚) ∩ {(𝐺𝑚)}) = ∅ ↔ ¬ (𝐺𝑚) ∈ (𝐺𝑚))
5957, 58sylibr 134 . . . . 5 ((𝑚 ∈ ℕ0 ∧ (1...𝑚) ≈ (𝐺𝑚)) → ((𝐺𝑚) ∩ {(𝐺𝑚)}) = ∅)
60 unen 6841 . . . . 5 ((((1...𝑚) ≈ (𝐺𝑚) ∧ {(𝑚 + 1)} ≈ {(𝐺𝑚)}) ∧ (((1...𝑚) ∩ {(𝑚 + 1)}) = ∅ ∧ ((𝐺𝑚) ∩ {(𝐺𝑚)}) = ∅)) → ((1...𝑚) ∪ {(𝑚 + 1)}) ≈ ((𝐺𝑚) ∪ {(𝐺𝑚)}))
6127, 47, 49, 59, 60syl22anc 1250 . . . 4 ((𝑚 ∈ ℕ0 ∧ (1...𝑚) ≈ (𝐺𝑚)) → ((1...𝑚) ∪ {(𝑚 + 1)}) ≈ ((𝐺𝑚) ∪ {(𝐺𝑚)}))
62 1z 9308 . . . . . 6 1 ∈ ℤ
63 1m1e0 9017 . . . . . . . . . 10 (1 − 1) = 0
6463fveq2i 5537 . . . . . . . . 9 (ℤ‘(1 − 1)) = (ℤ‘0)
6552, 64eqtr4i 2213 . . . . . . . 8 0 = (ℤ‘(1 − 1))
6665eleq2i 2256 . . . . . . 7 (𝑚 ∈ ℕ0𝑚 ∈ (ℤ‘(1 − 1)))
6766biimpi 120 . . . . . 6 (𝑚 ∈ ℕ0𝑚 ∈ (ℤ‘(1 − 1)))
68 fzsuc2 10108 . . . . . 6 ((1 ∈ ℤ ∧ 𝑚 ∈ (ℤ‘(1 − 1))) → (1...(𝑚 + 1)) = ((1...𝑚) ∪ {(𝑚 + 1)}))
6962, 67, 68sylancr 414 . . . . 5 (𝑚 ∈ ℕ0 → (1...(𝑚 + 1)) = ((1...𝑚) ∪ {(𝑚 + 1)}))
7069adantr 276 . . . 4 ((𝑚 ∈ ℕ0 ∧ (1...𝑚) ≈ (𝐺𝑚)) → (1...(𝑚 + 1)) = ((1...𝑚) ∪ {(𝑚 + 1)}))
71 peano2 4612 . . . . . . . . 9 ((𝐺𝑚) ∈ ω → suc (𝐺𝑚) ∈ ω)
7253, 71syl 14 . . . . . . . 8 (𝑚 ∈ ℕ0 → suc (𝐺𝑚) ∈ ω)
7372, 19jctil 312 . . . . . . 7 (𝑚 ∈ ℕ0 → (𝐺:ω–1-1-onto→(ℤ‘0) ∧ suc (𝐺𝑚) ∈ ω))
74 0zd 9294 . . . . . . . . . 10 ((𝐺𝑚) ∈ ω → 0 ∈ ℤ)
75 id 19 . . . . . . . . . 10 ((𝐺𝑚) ∈ ω → (𝐺𝑚) ∈ ω)
7674, 17, 75frec2uzsucd 10431 . . . . . . . . 9 ((𝐺𝑚) ∈ ω → (𝐺‘suc (𝐺𝑚)) = ((𝐺‘(𝐺𝑚)) + 1))
7753, 76syl 14 . . . . . . . 8 (𝑚 ∈ ℕ0 → (𝐺‘suc (𝐺𝑚)) = ((𝐺‘(𝐺𝑚)) + 1))
7852eleq2i 2256 . . . . . . . . . . 11 (𝑚 ∈ ℕ0𝑚 ∈ (ℤ‘0))
7978biimpi 120 . . . . . . . . . 10 (𝑚 ∈ ℕ0𝑚 ∈ (ℤ‘0))
80 f1ocnvfv2 5799 . . . . . . . . . 10 ((𝐺:ω–1-1-onto→(ℤ‘0) ∧ 𝑚 ∈ (ℤ‘0)) → (𝐺‘(𝐺𝑚)) = 𝑚)
8119, 79, 80sylancr 414 . . . . . . . . 9 (𝑚 ∈ ℕ0 → (𝐺‘(𝐺𝑚)) = 𝑚)
8281oveq1d 5910 . . . . . . . 8 (𝑚 ∈ ℕ0 → ((𝐺‘(𝐺𝑚)) + 1) = (𝑚 + 1))
8377, 82eqtrd 2222 . . . . . . 7 (𝑚 ∈ ℕ0 → (𝐺‘suc (𝐺𝑚)) = (𝑚 + 1))
84 f1ocnvfv 5800 . . . . . . 7 ((𝐺:ω–1-1-onto→(ℤ‘0) ∧ suc (𝐺𝑚) ∈ ω) → ((𝐺‘suc (𝐺𝑚)) = (𝑚 + 1) → (𝐺‘(𝑚 + 1)) = suc (𝐺𝑚)))
8573, 83, 84sylc 62 . . . . . 6 (𝑚 ∈ ℕ0 → (𝐺‘(𝑚 + 1)) = suc (𝐺𝑚))
8685adantr 276 . . . . 5 ((𝑚 ∈ ℕ0 ∧ (1...𝑚) ≈ (𝐺𝑚)) → (𝐺‘(𝑚 + 1)) = suc (𝐺𝑚))
87 df-suc 4389 . . . . 5 suc (𝐺𝑚) = ((𝐺𝑚) ∪ {(𝐺𝑚)})
8886, 87eqtrdi 2238 . . . 4 ((𝑚 ∈ ℕ0 ∧ (1...𝑚) ≈ (𝐺𝑚)) → (𝐺‘(𝑚 + 1)) = ((𝐺𝑚) ∪ {(𝐺𝑚)}))
8961, 70, 883brtr4d 4050 . . 3 ((𝑚 ∈ ℕ0 ∧ (1...𝑚) ≈ (𝐺𝑚)) → (1...(𝑚 + 1)) ≈ (𝐺‘(𝑚 + 1)))
9089ex 115 . 2 (𝑚 ∈ ℕ0 → ((1...𝑚) ≈ (𝐺𝑚) → (1...(𝑚 + 1)) ≈ (𝐺‘(𝑚 + 1))))
913, 6, 9, 12, 26, 90nn0ind 9396 1 (𝑁 ∈ ℕ0 → (1...𝑁) ≈ (𝐺𝑁))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wal 1362   = wceq 1364  wtru 1365  wcel 2160  Vcvv 2752  cun 3142  cin 3143  c0 3437  {csn 3607   class class class wbr 4018  cmpt 4079  Ord word 4380  suc csuc 4383  ωcom 4607  ccnv 4643   Fn wfn 5230  1-1-ontowf1o 5234  cfv 5235  (class class class)co 5895  freccfrec 6414  cen 6763  0cc0 7840  1c1 7841   + caddc 7843  cmin 8157  0cn0 9205  cz 9282  cuz 9557  ...cfz 10037
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 7931  ax-resscn 7932  ax-1cn 7933  ax-1re 7934  ax-icn 7935  ax-addcl 7936  ax-addrcl 7937  ax-mulcl 7938  ax-addcom 7940  ax-addass 7942  ax-distr 7944  ax-i2m1 7945  ax-0lt1 7946  ax-0id 7948  ax-rnegex 7949  ax-cnre 7951  ax-pre-ltirr 7952  ax-pre-ltwlin 7953  ax-pre-lttrn 7954  ax-pre-apti 7955  ax-pre-ltadd 7956
This theorem depends on definitions:  df-bi 117  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-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-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-riota 5851  df-ov 5898  df-oprab 5899  df-mpo 5900  df-recs 6329  df-frec 6415  df-1o 6440  df-er 6558  df-en 6766  df-pnf 8023  df-mnf 8024  df-xr 8025  df-ltxr 8026  df-le 8027  df-sub 8159  df-neg 8160  df-inn 8949  df-n0 9206  df-z 9283  df-uz 9558  df-fz 10038
This theorem is referenced by:  frecfzen2  10457  hashfz1  10794
  Copyright terms: Public domain W3C validator