Theorem frrlem6

Description: Lemma for well-founded recursion. The well-founded recursion generator is a relationship. (Contributed by Scott Fenton, 27-Aug-2022)

	Ref	Expression
Hypotheses	frrlem5.1	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
	frrlem5.2	⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
Assertion	frrlem6	⊢ Rel 𝐹

Proof

Step	Hyp	Ref	Expression
1		frrlem5.1	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
2		frrlem5.2	⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
3	1 2	frrlem5	⊢ 𝐹 = ∪ 𝐵
4	3	releqi	⊢ ( Rel 𝐹 ↔ Rel ∪ 𝐵 )
5		reluni	⊢ ( Rel ∪ 𝐵 ↔ ∀ 𝑔 ∈ 𝐵 Rel 𝑔 )
6	4 5	bitri	⊢ ( Rel 𝐹 ↔ ∀ 𝑔 ∈ 𝐵 Rel 𝑔 )
7	1	frrlem2	⊢ ( 𝑔 ∈ 𝐵 → Fun 𝑔 )
8		funrel	⊢ ( Fun 𝑔 → Rel 𝑔 )
9	7 8	syl	⊢ ( 𝑔 ∈ 𝐵 → Rel 𝑔 )
10	6 9	mprgbir	⊢ Rel 𝐹