Theorem rdglim 5320

Description: The value of the recursive definition generator at a limit ordinal.

Assertion

Ref	Expression
rdglim	|- ((B e. C /\ Lim B) -> (rec(F, A)` B) = U.(rec(F, A)"B))

Proof of Theorem rdglim

Step	Hyp	Ref	Expression
1		limelon 3873	. 2 |- ((B e. C /\ Lim B) -> B e. On)
2		limeq 3823	. . . . 5 |- (B = if(B e. On, B, (/)) -> (Lim B <-> Lim if(B e. On, B, (/))))
3		fveq2 4765	. . . . . 6 |- (B = if(B e. On, B, (/)) -> (rec(F, A)` B) = (rec(F, A)` if(B e. On, B, (/))))
4		imaeq2 4380	. . . . . . 7 |- (B = if(B e. On, B, (/)) -> (rec(F, A)"B) = (rec(F, A)"if(B e. On, B, (/))))
5	4	unieqd 3377	. . . . . 6 |- (B = if(B e. On, B, (/)) -> U.(rec(F, A)"B) = U.(rec(F, A)"if(B e. On, B, (/))))
6	3, 5	eqeq12d 2155	. . . . 5 |- (B = if(B e. On, B, (/)) -> ((rec(F, A)` B) = U.(rec(F, A)"B) <-> (rec(F, A)` if(B e. On, B, (/))) = U.(rec(F, A)"if(B e. On, B, (/)))))
7	2, 6	imbi12d 761	. . . 4 |- (B = if(B e. On, B, (/)) -> ((Lim B -> (rec(F, A)` B) = U.(rec(F, A)"B)) <-> (Lim if(B e. On, B, (/)) -> (rec(F, A)` if(B e. On, B, (/))) = U.(rec(F, A)"if(B e. On, B, (/))))))
8		0elon 3863	. . . . . 6 |- (/) e. On
9	8	elimel 3219	. . . . 5 |- if(B e. On, B, (/)) e. On
10	9	rdglimi 5315	. . . 4 |- (Lim if(B e. On, B, (/)) -> (rec(F, A)` if(B e. On, B, (/))) = U.(rec(F, A)"if(B e. On, B, (/))))
11	7, 10	dedth 3208	. . 3 |- (B e. On -> (Lim B -> (rec(F, A)` B) = U.(rec(F, A)"B)))
12	11	imp 393	. 2 |- ((B e. On /\ Lim B) -> (rec(F, A)` B) = U.(rec(F, A)"B))
13	1, 12	sylancom 670	1 |- ((B e. C /\ Lim B) -> (rec(F, A)` B) = U.(rec(F, A)"B))

Syntax hints:   -> wi 3   /\ wa 337   = wceq 1586   e. wcel 1588  (/)c0 3082  ifcif 3180  U.cuni 3366  Oncon0 3811  Lim wlim 3812  "cima 4122  ` cfv 4131  reccrdg 5303

This theorem is referenced by:  rdglim2 5321  vtarl 16074

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-ral 2359  df-rex 2360  df-rab 2362  df-v 2540  df-sbc 2700  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-if 3181  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-iun 3438  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-id 3747  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-lim 3816  df-suc 3817  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-fv 4147  df-rdg 5304

Copyright terms: Public domain