Metamath Proof Explorer


Theorem rdg0n

Description: If A is a proper class, then the recursive function generator at (/) is the empty set. (Contributed by Scott Fenton, 31-Oct-2024)

Ref Expression
Assertion rdg0n ¬AVrecFA=

Proof

Step Hyp Ref Expression
1 0elon On
2 df-rdg recFA=recsgVifg=AifLimdomgrangFgdomg
3 2 tfr2 OnrecFA=gVifg=AifLimdomgrangFgdomgrecFA
4 1 3 ax-mp recFA=gVifg=AifLimdomgrangFgdomgrecFA
5 res0 recFA=
6 5 fveq2i gVifg=AifLimdomgrangFgdomgrecFA=gVifg=AifLimdomgrangFgdomg
7 4 6 eqtri recFA=gVifg=AifLimdomgrangFgdomg
8 iftrue g=ifg=AifLimdomgrangFgdomg=A
9 eqid gVifg=AifLimdomgrangFgdomg=gVifg=AifLimdomgrangFgdomg
10 8 9 fvmptn ¬AVgVifg=AifLimdomgrangFgdomg=
11 7 10 eqtrid ¬AVrecFA=