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

Theorem rdgi0g 5882
 Description: The initial value of the recursive definition generator. (Contributed by Jim Kingdon, 10-Jul-2019.)
Assertion
Ref Expression
rdgi0g ((𝐹 Fn V A 𝑉) → (rec(𝐹, A)‘∅) = A)

Proof of Theorem rdgi0g
Dummy variables g x y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0elon 4074 . . . . 5 On
2 df-irdg 5874 . . . . . 6 rec(𝐹, A) = recs((g V ↦ (A x dom g(𝐹‘(gx)))))
3 rdgruledefgg 5878 . . . . . . 7 ((𝐹 Fn V A 𝑉) → (Fun (g V ↦ (A x dom g(𝐹‘(gx)))) ((g V ↦ (A x dom g(𝐹‘(gx))))‘y) V))
43alrimiv 1732 . . . . . 6 ((𝐹 Fn V A 𝑉) → y(Fun (g V ↦ (A x dom g(𝐹‘(gx)))) ((g V ↦ (A x dom g(𝐹‘(gx))))‘y) V))
52, 4tfri2d 5868 . . . . 5 (((𝐹 Fn V A 𝑉) On) → (rec(𝐹, A)‘∅) = ((g V ↦ (A x dom g(𝐹‘(gx))))‘(rec(𝐹, A) ↾ ∅)))
61, 5mpan2 403 . . . 4 ((𝐹 Fn V A 𝑉) → (rec(𝐹, A)‘∅) = ((g V ↦ (A x dom g(𝐹‘(gx))))‘(rec(𝐹, A) ↾ ∅)))
7 res0 4539 . . . . 5 (rec(𝐹, A) ↾ ∅) = ∅
87fveq2i 5102 . . . 4 ((g V ↦ (A x dom g(𝐹‘(gx))))‘(rec(𝐹, A) ↾ ∅)) = ((g V ↦ (A x dom g(𝐹‘(gx))))‘∅)
96, 8syl6eq 2066 . . 3 ((𝐹 Fn V A 𝑉) → (rec(𝐹, A)‘∅) = ((g V ↦ (A x dom g(𝐹‘(gx))))‘∅))
10 0ex 3854 . . . 4 V
1110dmex 4521 . . . . . 6 dom ∅ V
12 0fv 5129 . . . . . . . . 9 (∅‘x) = ∅
1312fveq2i 5102 . . . . . . . 8 (𝐹‘(∅‘x)) = (𝐹‘∅)
14 funfvex 5113 . . . . . . . . . 10 ((Fun 𝐹 dom 𝐹) → (𝐹‘∅) V)
1514funfni 4921 . . . . . . . . 9 ((𝐹 Fn V V) → (𝐹‘∅) V)
1610, 15mpan2 403 . . . . . . . 8 (𝐹 Fn V → (𝐹‘∅) V)
1713, 16syl5eqel 2102 . . . . . . 7 (𝐹 Fn V → (𝐹‘(∅‘x)) V)
1817ralrimivw 2367 . . . . . 6 (𝐹 Fn V → x dom ∅(𝐹‘(∅‘x)) V)
19 iunexg 5665 . . . . . 6 ((dom ∅ V x dom ∅(𝐹‘(∅‘x)) V) → x dom ∅(𝐹‘(∅‘x)) V)
2011, 18, 19sylancr 395 . . . . 5 (𝐹 Fn V → x dom ∅(𝐹‘(∅‘x)) V)
21 unexg 4124 . . . . . 6 ((A 𝑉 x dom ∅(𝐹‘(∅‘x)) V) → (A x dom ∅(𝐹‘(∅‘x))) V)
2221ex 108 . . . . 5 (A 𝑉 → ( x dom ∅(𝐹‘(∅‘x)) V → (A x dom ∅(𝐹‘(∅‘x))) V))
2320, 22mpan9 265 . . . 4 ((𝐹 Fn V A 𝑉) → (A x dom ∅(𝐹‘(∅‘x))) V)
24 dmeq 4458 . . . . . . 7 (g = ∅ → dom g = dom ∅)
25 fveq1 5098 . . . . . . . 8 (g = ∅ → (gx) = (∅‘x))
2625fveq2d 5103 . . . . . . 7 (g = ∅ → (𝐹‘(gx)) = (𝐹‘(∅‘x)))
2724, 26iuneq12d 3651 . . . . . 6 (g = ∅ → x dom g(𝐹‘(gx)) = x dom ∅(𝐹‘(∅‘x)))
2827uneq2d 3070 . . . . 5 (g = ∅ → (A x dom g(𝐹‘(gx))) = (A x dom ∅(𝐹‘(∅‘x))))
29 eqid 2018 . . . . 5 (g V ↦ (A x dom g(𝐹‘(gx)))) = (g V ↦ (A x dom g(𝐹‘(gx))))
3028, 29fvmptg 5169 . . . 4 ((∅ V (A x dom ∅(𝐹‘(∅‘x))) V) → ((g V ↦ (A x dom g(𝐹‘(gx))))‘∅) = (A x dom ∅(𝐹‘(∅‘x))))
3110, 23, 30sylancr 395 . . 3 ((𝐹 Fn V A 𝑉) → ((g V ↦ (A x dom g(𝐹‘(gx))))‘∅) = (A x dom ∅(𝐹‘(∅‘x))))
329, 31eqtrd 2050 . 2 ((𝐹 Fn V A 𝑉) → (rec(𝐹, A)‘∅) = (A x dom ∅(𝐹‘(∅‘x))))
33 dm0 4472 . . . . . 6 dom ∅ = ∅
34 iuneq1 3640 . . . . . 6 (dom ∅ = ∅ → x dom ∅(𝐹‘(∅‘x)) = x ∅ (𝐹‘(∅‘x)))
3533, 34ax-mp 7 . . . . 5 x dom ∅(𝐹‘(∅‘x)) = x ∅ (𝐹‘(∅‘x))
36 0iun 3684 . . . . 5 x ∅ (𝐹‘(∅‘x)) = ∅
3735, 36eqtri 2038 . . . 4 x dom ∅(𝐹‘(∅‘x)) = ∅
3837uneq2i 3067 . . 3 (A x dom ∅(𝐹‘(∅‘x))) = (A ∪ ∅)
39 un0 3224 . . 3 (A ∪ ∅) = A
4038, 39eqtri 2038 . 2 (A x dom ∅(𝐹‘(∅‘x))) = A
4132, 40syl6eq 2066 1 ((𝐹 Fn V A 𝑉) → (rec(𝐹, A)‘∅) = A)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   = wceq 1226   ∈ wcel 1370  ∀wral 2280  Vcvv 2531   ∪ cun 2888  ∅c0 3197  ∪ ciun 3627   ↦ cmpt 3788  Oncon0 4045  dom cdm 4268   ↾ cres 4270  Fun wfun 4819   Fn wfn 4820  ‘cfv 4825  reccrdg 5873 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 532  ax-in2 533  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-13 1381  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-coll 3842  ax-sep 3845  ax-nul 3853  ax-pow 3897  ax-pr 3914  ax-un 4116  ax-setind 4200 This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-fal 1232  df-nf 1326  df-sb 1624  df-eu 1881  df-mo 1882  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ne 2184  df-ral 2285  df-rex 2286  df-reu 2287  df-rab 2289  df-v 2533  df-sbc 2738  df-csb 2826  df-dif 2893  df-un 2895  df-in 2897  df-ss 2904  df-nul 3198  df-pw 3332  df-sn 3352  df-pr 3353  df-op 3355  df-uni 3551  df-iun 3629  df-br 3735  df-opab 3789  df-mpt 3790  df-tr 3825  df-id 4000  df-iord 4048  df-on 4050  df-suc 4053  df-xp 4274  df-rel 4275  df-cnv 4276  df-co 4277  df-dm 4278  df-rn 4279  df-res 4280  df-ima 4281  df-iota 4790  df-fun 4827  df-fn 4828  df-f 4829  df-f1 4830  df-fo 4831  df-f1o 4832  df-fv 4833  df-recs 5838  df-irdg 5874 This theorem is referenced by:  frecrdg  5904  oa0  5948  om0  5949  oei0  5950
 Copyright terms: Public domain W3C validator