My understanding is that it stands for "founded relation", as in
well-founded but without the "well", I think because it doesn't have any
other ordering properties like being a partial order attached to it.
On Wed, May 1, 2024 at 5:21 AM 'B. Wilson' via Metamath <
metamath@googlegroups.com>
This has been bugging me midly for a while, but I couldn't figure out what the
Fr symbol in df-fr stood for:
19201 df-fr $a |- ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x
A. z e. x -. z R y ) ) $.
I finally bothered to look up the Takeuti and Zaring reference, which also uses
