Metamath Proof Explorer

Theorem frrrel

Description: Show without using the axiom of replacement that the well-founded recursion generator gives a relation. (Contributed by Scott Fenton, 18-Nov-2024)

		Ref	Expression
	Hypothesis	frrrel.1	\|- F = frecs ( R , A , G )
	Assertion	frrrel	\|- Rel F

Proof

Step	Hyp	Ref	Expression
1		frrrel.1	\|- F = frecs ( R , A , G )
2		eqid	\|- { f \| E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( y G ( f \|` Pred ( R , A , y ) ) ) ) } = { f \| E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( y G ( f \|` Pred ( R , A , y ) ) ) ) }
3	2 1	frrlem6	\|- Rel F

Step

Hyp

Ref

Expression

frrrel.1

 |-  F = frecs ( R , A , G )

eqid

 |-  { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( y G ( f |` Pred ( R , A , y ) ) ) ) } = { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( y G ( f |` Pred ( R , A , y ) ) ) ) }

2 1

frrlem6

 |-  Rel F