Metamath Proof Explorer


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 ( 𝑅 , 𝐴 , 𝑋 ) ) ) )