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 \in dom F \to Pred (R, A, X) \subseteq dom F$

Proof

Step	Hyp	Ref	Expression
1		frrrel.1	$⊢ F = frecs (R, A, G)$
2		predeq3	$⊢ z = X \to Pred (R, A, z) = Pred (R, A, X)$
3	2	sseq1d	$⊢ z = X \to (Pred (R, A, z) \subseteq dom F \leftrightarrow Pred (R, A, X) \subseteq dom F)$
4		eqid	$⊢ \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = y G ({f ↾}_{Pred (R, A, y)}))\} = \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = y G ({f ↾}_{Pred (R, A, y)}))\}$
5	4 1	frrlem8	$⊢ z \in dom F \to Pred (R, A, z) \subseteq dom F$
6	3 5	vtoclga	$⊢ X \in dom F \to Pred (R, A, X) \subseteq dom F$

Metamath Proof Explorer

Theorem frrdmcl

Proof