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	⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
Assertion	frrrel	⊢ Rel 𝐹

Proof

Step	Hyp	Ref	Expression
1		frrrel.1	⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
2		eqid	⊢ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
3	2 1	frrlem6	⊢ Rel 𝐹