Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  rdglim2 Structured version   Unicode version

Theorem rdglim2 7161
 Description: The value of the recursive definition generator at a limit ordinal, in terms of the union of all smaller values. (Contributed by NM, 23-Apr-1995.)
Assertion
Ref Expression
rdglim2
Distinct variable groups:   ,,   ,,   ,,
Allowed substitution hints:   (,)

Proof of Theorem rdglim2
StepHypRef Expression
1 rdglim 7155 . 2
2 dfima3 5190 . . . . 5
3 df-rex 2777 . . . . . . 7
4 limord 5501 . . . . . . . . . . 11
5 ordelord 5464 . . . . . . . . . . . . 13
65ex 435 . . . . . . . . . . . 12
7 vex 3083 . . . . . . . . . . . . 13
87elon 5451 . . . . . . . . . . . 12
96, 8syl6ibr 230 . . . . . . . . . . 11
104, 9syl 17 . . . . . . . . . 10
11 eqcom 2431 . . . . . . . . . . 11
12 rdgfnon 7147 . . . . . . . . . . . 12
13 fnopfvb 5922 . . . . . . . . . . . 12
1412, 13mpan 674 . . . . . . . . . . 11
1511, 14syl5bb 260 . . . . . . . . . 10
1610, 15syl6 34 . . . . . . . . 9
1716pm5.32d 643 . . . . . . . 8
1817exbidv 1762 . . . . . . 7
193, 18syl5rbb 261 . . . . . 6
2019abbidv 2553 . . . . 5
212, 20syl5eq 2475 . . . 4
2221unieqd 4229 . . 3