Transitive closure help

[Scott Fenton]

Hi all,

I'm working on founded recursion (recursion when R Fr A as opposed to R We A) and I'm encountering some machinery trouble.  Specifically, I'd like to use +c to prove a bunch of properties, but my relationships may be proper classes.  Furthermore, I'd like the logic to be prior to the real numbers, as I'm going to use it in my surreal number development, which logically contains an isomorphic set of reals.  I'm using df-trpred at the moment to work around it, but that's clunky.  Anyone have any definitional ideas I could go on here?

Thanks,

Scott