Theorem fpr2

Description: Law of well-founded recursion over a partial order, part two. Now we establish the value of F within A . (Contributed by Scott Fenton, 11-Sep-2023) (Proof shortened by Scott Fenton, 18-Nov-2024)

	Ref	Expression
Hypothesis	fprr.1	⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
Assertion	fpr2	⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝑋 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fprr.1	⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
2	1	fpr1	⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝐹 Fn 𝐴 )
3	2	fndmd	⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → dom 𝐹 = 𝐴 )
4	3	eleq2d	⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑋 ∈ dom 𝐹 ↔ 𝑋 ∈ 𝐴 ) )
5	4	biimpar	⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ dom 𝐹 )
6	1	fpr2a	⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝑋 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) )
7	5 6	syldan	⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝑋 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) )