Metamath Proof Explorer


Theorem rdgprc0

Description: The value of the recursive definition generator at (/) when the base value is a proper class. (Contributed by Scott Fenton, 26-Mar-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion rdgprc0 ¬ I V rec F I =

Proof

Step Hyp Ref Expression
1 0elon On
2 rdgval On rec F I = g V if g = I if Lim dom g ran g F g dom g rec F I
3 1 2 ax-mp rec F I = g V if g = I if Lim dom g ran g F g dom g rec F I
4 res0 rec F I =
5 4 fveq2i g V if g = I if Lim dom g ran g F g dom g rec F I = g V if g = I if Lim dom g ran g F g dom g
6 3 5 eqtri rec F I = g V if g = I if Lim dom g ran g F g dom g
7 eqeq1 g = g = =
8 dmeq g = dom g = dom
9 limeq dom g = dom Lim dom g Lim dom
10 8 9 syl g = Lim dom g Lim dom
11 rneq g = ran g = ran
12 11 unieqd g = ran g = ran
13 id g = g =
14 8 unieqd g = dom g = dom
15 13 14 fveq12d g = g dom g = dom
16 15 fveq2d g = F g dom g = F dom
17 10 12 16 ifbieq12d g = if Lim dom g ran g F g dom g = if Lim dom ran F dom
18 7 17 ifbieq2d g = if g = I if Lim dom g ran g F g dom g = if = I if Lim dom ran F dom
19 18 eleq1d g = if g = I if Lim dom g ran g F g dom g V if = I if Lim dom ran F dom V
20 eqid g V if g = I if Lim dom g ran g F g dom g = g V if g = I if Lim dom g ran g F g dom g
21 20 dmmpt dom g V if g = I if Lim dom g ran g F g dom g = g V | if g = I if Lim dom g ran g F g dom g V
22 19 21 elrab2 dom g V if g = I if Lim dom g ran g F g dom g V if = I if Lim dom ran F dom V
23 eqid =
24 23 iftruei if = I if Lim dom ran F dom = I
25 24 eleq1i if = I if Lim dom ran F dom V I V
26 25 biimpi if = I if Lim dom ran F dom V I V
27 22 26 simplbiim dom g V if g = I if Lim dom g ran g F g dom g I V
28 ndmfv ¬ dom g V if g = I if Lim dom g ran g F g dom g g V if g = I if Lim dom g ran g F g dom g =
29 27 28 nsyl5 ¬ I V g V if g = I if Lim dom g ran g F g dom g =
30 6 29 syl5eq ¬ I V rec F I =