Metamath Proof Explorer

Theorem frrdmss

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

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

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	frrlem7	\|- dom F C_ A

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

frrlem7

 |-  dom F C_ A