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