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

Theorem frec0g 6200
Description: The initial value resulting from finite recursive definition generation. (Contributed by Jim Kingdon, 7-May-2020.)
Assertion
Ref Expression
frec0g (𝐴𝑉 → (frec(𝐹, 𝐴)‘∅) = 𝐴)

Proof of Theorem frec0g
Dummy variables 𝑔 𝑚 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dm0 4681 . . . . . . . . . 10 dom ∅ = ∅
21biantrur 298 . . . . . . . . 9 (𝑥𝐴 ↔ (dom ∅ = ∅ ∧ 𝑥𝐴))
3 vex 2636 . . . . . . . . . . . . . . . 16 𝑚 ∈ V
4 nsuceq0g 4269 . . . . . . . . . . . . . . . 16 (𝑚 ∈ V → suc 𝑚 ≠ ∅)
53, 4ax-mp 7 . . . . . . . . . . . . . . 15 suc 𝑚 ≠ ∅
65nesymi 2308 . . . . . . . . . . . . . 14 ¬ ∅ = suc 𝑚
71eqeq1i 2102 . . . . . . . . . . . . . 14 (dom ∅ = suc 𝑚 ↔ ∅ = suc 𝑚)
86, 7mtbir 634 . . . . . . . . . . . . 13 ¬ dom ∅ = suc 𝑚
98intnanr 880 . . . . . . . . . . . 12 ¬ (dom ∅ = suc 𝑚𝑥 ∈ (𝐹‘(∅‘𝑚)))
109a1i 9 . . . . . . . . . . 11 (𝑚 ∈ ω → ¬ (dom ∅ = suc 𝑚𝑥 ∈ (𝐹‘(∅‘𝑚))))
1110nrex 2477 . . . . . . . . . 10 ¬ ∃𝑚 ∈ ω (dom ∅ = suc 𝑚𝑥 ∈ (𝐹‘(∅‘𝑚)))
1211biorfi 703 . . . . . . . . 9 ((dom ∅ = ∅ ∧ 𝑥𝐴) ↔ ((dom ∅ = ∅ ∧ 𝑥𝐴) ∨ ∃𝑚 ∈ ω (dom ∅ = suc 𝑚𝑥 ∈ (𝐹‘(∅‘𝑚)))))
13 orcom 685 . . . . . . . . 9 (((dom ∅ = ∅ ∧ 𝑥𝐴) ∨ ∃𝑚 ∈ ω (dom ∅ = suc 𝑚𝑥 ∈ (𝐹‘(∅‘𝑚)))) ↔ (∃𝑚 ∈ ω (dom ∅ = suc 𝑚𝑥 ∈ (𝐹‘(∅‘𝑚))) ∨ (dom ∅ = ∅ ∧ 𝑥𝐴)))
142, 12, 133bitri 205 . . . . . . . 8 (𝑥𝐴 ↔ (∃𝑚 ∈ ω (dom ∅ = suc 𝑚𝑥 ∈ (𝐹‘(∅‘𝑚))) ∨ (dom ∅ = ∅ ∧ 𝑥𝐴)))
1514abbii 2210 . . . . . . 7 {𝑥𝑥𝐴} = {𝑥 ∣ (∃𝑚 ∈ ω (dom ∅ = suc 𝑚𝑥 ∈ (𝐹‘(∅‘𝑚))) ∨ (dom ∅ = ∅ ∧ 𝑥𝐴))}
16 abid2 2215 . . . . . . 7 {𝑥𝑥𝐴} = 𝐴
1715, 16eqtr3i 2117 . . . . . 6 {𝑥 ∣ (∃𝑚 ∈ ω (dom ∅ = suc 𝑚𝑥 ∈ (𝐹‘(∅‘𝑚))) ∨ (dom ∅ = ∅ ∧ 𝑥𝐴))} = 𝐴
18 elex 2644 . . . . . 6 (𝐴𝑉𝐴 ∈ V)
1917, 18syl5eqel 2181 . . . . 5 (𝐴𝑉 → {𝑥 ∣ (∃𝑚 ∈ ω (dom ∅ = suc 𝑚𝑥 ∈ (𝐹‘(∅‘𝑚))) ∨ (dom ∅ = ∅ ∧ 𝑥𝐴))} ∈ V)
20 0ex 3987 . . . . . . 7 ∅ ∈ V
21 dmeq 4667 . . . . . . . . . . . . 13 (𝑔 = ∅ → dom 𝑔 = dom ∅)
2221eqeq1d 2103 . . . . . . . . . . . 12 (𝑔 = ∅ → (dom 𝑔 = suc 𝑚 ↔ dom ∅ = suc 𝑚))
23 fveq1 5339 . . . . . . . . . . . . . 14 (𝑔 = ∅ → (𝑔𝑚) = (∅‘𝑚))
2423fveq2d 5344 . . . . . . . . . . . . 13 (𝑔 = ∅ → (𝐹‘(𝑔𝑚)) = (𝐹‘(∅‘𝑚)))
2524eleq2d 2164 . . . . . . . . . . . 12 (𝑔 = ∅ → (𝑥 ∈ (𝐹‘(𝑔𝑚)) ↔ 𝑥 ∈ (𝐹‘(∅‘𝑚))))
2622, 25anbi12d 458 . . . . . . . . . . 11 (𝑔 = ∅ → ((dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ↔ (dom ∅ = suc 𝑚𝑥 ∈ (𝐹‘(∅‘𝑚)))))
2726rexbidv 2392 . . . . . . . . . 10 (𝑔 = ∅ → (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ↔ ∃𝑚 ∈ ω (dom ∅ = suc 𝑚𝑥 ∈ (𝐹‘(∅‘𝑚)))))
2821eqeq1d 2103 . . . . . . . . . . 11 (𝑔 = ∅ → (dom 𝑔 = ∅ ↔ dom ∅ = ∅))
2928anbi1d 454 . . . . . . . . . 10 (𝑔 = ∅ → ((dom 𝑔 = ∅ ∧ 𝑥𝐴) ↔ (dom ∅ = ∅ ∧ 𝑥𝐴)))
3027, 29orbi12d 745 . . . . . . . . 9 (𝑔 = ∅ → ((∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴)) ↔ (∃𝑚 ∈ ω (dom ∅ = suc 𝑚𝑥 ∈ (𝐹‘(∅‘𝑚))) ∨ (dom ∅ = ∅ ∧ 𝑥𝐴))))
3130abbidv 2212 . . . . . . . 8 (𝑔 = ∅ → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))} = {𝑥 ∣ (∃𝑚 ∈ ω (dom ∅ = suc 𝑚𝑥 ∈ (𝐹‘(∅‘𝑚))) ∨ (dom ∅ = ∅ ∧ 𝑥𝐴))})
32 eqid 2095 . . . . . . . 8 (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))}) = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})
3331, 32fvmptg 5415 . . . . . . 7 ((∅ ∈ V ∧ {𝑥 ∣ (∃𝑚 ∈ ω (dom ∅ = suc 𝑚𝑥 ∈ (𝐹‘(∅‘𝑚))) ∨ (dom ∅ = ∅ ∧ 𝑥𝐴))} ∈ V) → ((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})‘∅) = {𝑥 ∣ (∃𝑚 ∈ ω (dom ∅ = suc 𝑚𝑥 ∈ (𝐹‘(∅‘𝑚))) ∨ (dom ∅ = ∅ ∧ 𝑥𝐴))})
3420, 33mpan 416 . . . . . 6 ({𝑥 ∣ (∃𝑚 ∈ ω (dom ∅ = suc 𝑚𝑥 ∈ (𝐹‘(∅‘𝑚))) ∨ (dom ∅ = ∅ ∧ 𝑥𝐴))} ∈ V → ((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})‘∅) = {𝑥 ∣ (∃𝑚 ∈ ω (dom ∅ = suc 𝑚𝑥 ∈ (𝐹‘(∅‘𝑚))) ∨ (dom ∅ = ∅ ∧ 𝑥𝐴))})
3534, 17syl6eq 2143 . . . . 5 ({𝑥 ∣ (∃𝑚 ∈ ω (dom ∅ = suc 𝑚𝑥 ∈ (𝐹‘(∅‘𝑚))) ∨ (dom ∅ = ∅ ∧ 𝑥𝐴))} ∈ V → ((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})‘∅) = 𝐴)
3619, 35syl 14 . . . 4 (𝐴𝑉 → ((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})‘∅) = 𝐴)
3736, 18eqeltrd 2171 . . 3 (𝐴𝑉 → ((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})‘∅) ∈ V)
38 df-frec 6194 . . . . . 6 frec(𝐹, 𝐴) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})) ↾ ω)
3938fveq1i 5341 . . . . 5 (frec(𝐹, 𝐴)‘∅) = ((recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})) ↾ ω)‘∅)
40 peano1 4437 . . . . . 6 ∅ ∈ ω
41 fvres 5364 . . . . . 6 (∅ ∈ ω → ((recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})) ↾ ω)‘∅) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))}))‘∅))
4240, 41ax-mp 7 . . . . 5 ((recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})) ↾ ω)‘∅) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))}))‘∅)
4339, 42eqtri 2115 . . . 4 (frec(𝐹, 𝐴)‘∅) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))}))‘∅)
44 eqid 2095 . . . . 5 recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})) = recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))}))
4544tfr0 6126 . . . 4 (((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})‘∅) ∈ V → (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))}))‘∅) = ((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})‘∅))
4643, 45syl5eq 2139 . . 3 (((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})‘∅) ∈ V → (frec(𝐹, 𝐴)‘∅) = ((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})‘∅))
4737, 46syl 14 . 2 (𝐴𝑉 → (frec(𝐹, 𝐴)‘∅) = ((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})‘∅))
4847, 36eqtrd 2127 1 (𝐴𝑉 → (frec(𝐹, 𝐴)‘∅) = 𝐴)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wo 667   = wceq 1296  wcel 1445  {cab 2081  wne 2262  wrex 2371  Vcvv 2633  c0 3302  cmpt 3921  suc csuc 4216  ωcom 4433  dom cdm 4467  cres 4469  cfv 5049  recscrecs 6107  freccfrec 6193
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 582  ax-in2 583  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-13 1456  ax-14 1457  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-sep 3978  ax-nul 3986  ax-pow 4030  ax-pr 4060  ax-un 4284  ax-setind 4381
This theorem depends on definitions:  df-bi 116  df-3an 929  df-tru 1299  df-fal 1302  df-nf 1402  df-sb 1700  df-eu 1958  df-mo 1959  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ne 2263  df-ral 2375  df-rex 2376  df-rab 2379  df-v 2635  df-sbc 2855  df-csb 2948  df-dif 3015  df-un 3017  df-in 3019  df-ss 3026  df-nul 3303  df-pw 3451  df-sn 3472  df-pr 3473  df-op 3475  df-uni 3676  df-int 3711  df-iun 3754  df-br 3868  df-opab 3922  df-mpt 3923  df-tr 3959  df-id 4144  df-iord 4217  df-on 4219  df-suc 4222  df-iom 4434  df-xp 4473  df-rel 4474  df-cnv 4475  df-co 4476  df-dm 4477  df-res 4479  df-iota 5014  df-fun 5051  df-fn 5052  df-fv 5057  df-recs 6108  df-frec 6194
This theorem is referenced by:  frecrdg  6211  frec2uz0d  9955  frec2uzrdg  9965  frecuzrdg0  9969  frecuzrdgg  9972  frecuzrdg0t  9978  iseqvalt  10019  seq3val  10020
  Copyright terms: Public domain W3C validator