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

Theorem rdg0 5891
 Description: The initial value of the recursive definition generator. (Contributed by NM, 23-Apr-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
Hypotheses
Ref Expression
rdg0.1 A V
rdg0.2 𝐹 Fn V
Assertion
Ref Expression
rdg0 (rec(𝐹, A)‘∅) = A

Proof of Theorem rdg0
Dummy variables x y g 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 rdg0.1 . . . . . . 7 A V
4 rdg0.2 . . . . . . 7 𝐹 Fn V
53, 4rdgruledef 5890 . . . . . 6 (Fun (g V ↦ (A x dom g(𝐹‘(gx)))) ((g V ↦ (A x dom g(𝐹‘(gx))))‘y) V)
62, 5tfri2 5870 . . . . 5 (∅ On → (rec(𝐹, A)‘∅) = ((g V ↦ (A x dom g(𝐹‘(gx))))‘(rec(𝐹, A) ↾ ∅)))
71, 6ax-mp 7 . . . 4 (rec(𝐹, A)‘∅) = ((g V ↦ (A x dom g(𝐹‘(gx))))‘(rec(𝐹, A) ↾ ∅))
8 res0 4539 . . . . 5 (rec(𝐹, A) ↾ ∅) = ∅
98fveq2i 5102 . . . 4 ((g V ↦ (A x dom g(𝐹‘(gx))))‘(rec(𝐹, A) ↾ ∅)) = ((g V ↦ (A x dom g(𝐹‘(gx))))‘∅)
107, 9eqtri 2038 . . 3 (rec(𝐹, A)‘∅) = ((g V ↦ (A x dom g(𝐹‘(gx))))‘∅)
11 0ex 3854 . . . 4 V
12 dmeq 4458 . . . . . . 7 (g = ∅ → dom g = dom ∅)
13 fveq1 5098 . . . . . . . 8 (g = ∅ → (gx) = (∅‘x))
1413fveq2d 5103 . . . . . . 7 (g = ∅ → (𝐹‘(gx)) = (𝐹‘(∅‘x)))
1512, 14iuneq12d 3651 . . . . . 6 (g = ∅ → x dom g(𝐹‘(gx)) = x dom ∅(𝐹‘(∅‘x)))
1615uneq2d 3070 . . . . 5 (g = ∅ → (A x dom g(𝐹‘(gx))) = (A x dom ∅(𝐹‘(∅‘x))))
17 eqid 2018 . . . . 5 (g V ↦ (A x dom g(𝐹‘(gx)))) = (g V ↦ (A x dom g(𝐹‘(gx))))
1811dmex 4521 . . . . . . 7 dom ∅ V
19 0fv 5129 . . . . . . . . 9 (∅‘x) = ∅
2019fveq2i 5102 . . . . . . . 8 (𝐹‘(∅‘x)) = (𝐹‘∅)
21 funfvex 5113 . . . . . . . . . 10 ((Fun 𝐹 dom 𝐹) → (𝐹‘∅) V)
2221funfni 4921 . . . . . . . . 9 ((𝐹 Fn V V) → (𝐹‘∅) V)
234, 11, 22mp2an 404 . . . . . . . 8 (𝐹‘∅) V
2420, 23eqeltri 2088 . . . . . . 7 (𝐹‘(∅‘x)) V
2518, 24iunex 5669 . . . . . 6 x dom ∅(𝐹‘(∅‘x)) V
263, 25unex 4122 . . . . 5 (A x dom ∅(𝐹‘(∅‘x))) V
2716, 17, 26fvmpt 5170 . . . 4 (∅ V → ((g V ↦ (A x dom g(𝐹‘(gx))))‘∅) = (A x dom ∅(𝐹‘(∅‘x))))
2811, 27ax-mp 7 . . 3 ((g V ↦ (A x dom g(𝐹‘(gx))))‘∅) = (A x dom ∅(𝐹‘(∅‘x)))
2910, 28eqtri 2038 . 2 (rec(𝐹, A)‘∅) = (A x dom ∅(𝐹‘(∅‘x)))
30 dm0 4472 . . . . . 6 dom ∅ = ∅
31 iuneq1 3640 . . . . . 6 (dom ∅ = ∅ → x dom ∅(𝐹‘(∅‘x)) = x ∅ (𝐹‘(∅‘x)))
3230, 31ax-mp 7 . . . . 5 x dom ∅(𝐹‘(∅‘x)) = x ∅ (𝐹‘(∅‘x))
33 0iun 3684 . . . . 5 x ∅ (𝐹‘(∅‘x)) = ∅
3432, 33eqtri 2038 . . . 4 x dom ∅(𝐹‘(∅‘x)) = ∅
3534uneq2i 3067 . . 3 (A x dom ∅(𝐹‘(∅‘x))) = (A ∪ ∅)
36 un0 3224 . . 3 (A ∪ ∅) = A
3735, 36eqtri 2038 . 2 (A x dom ∅(𝐹‘(∅‘x))) = A
3829, 37eqtri 2038 1 (rec(𝐹, A)‘∅) = A
 Colors of variables: wff set class Syntax hints:   = wceq 1226   ∈ wcel 1370  Vcvv 2531   ∪ cun 2888  ∅c0 3197  ∪ ciun 3627   ↦ cmpt 3788  Oncon0 4045  dom cdm 4268   ↾ cres 4270   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: (None)
 Copyright terms: Public domain W3C validator