Theorem frrdmcl

Description: Show without using the axiom of replacement that for a "function" defined by well-founded recursion, the predecessor class of an element of its domain is a subclass of its domain. (Contributed by Scott Fenton, 21-Apr-2011) (Proof shortened by Scott Fenton, 17-Nov-2024)

	Ref	Expression
Hypothesis	frrrel.1	|- F = frecs ( R , A , G )
Assertion	frrdmcl	|- ( X e. dom F -> Pred ( R , A , X ) C_ dom F )

Proof

Step	Hyp	Ref	Expression
1		frrrel.1	|- F = frecs ( R , A , G )
2		predeq3	|- ( z = X -> Pred ( R , A , z ) = Pred ( R , A , X ) )
3	2	sseq1d	|- ( z = X -> ( Pred ( R , A , z ) C_ dom F <-> Pred ( R , A , X ) C_ dom F ) )
4		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 ) ) ) ) }
5	4 1	frrlem8	|- ( z e. dom F -> Pred ( R , A , z ) C_ dom F )
6	3 5	vtoclga	|- ( X e. dom F -> Pred ( R , A , X ) C_ dom F )