Step |
Hyp |
Ref |
Expression |
1 |
|
fprr.1 |
⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 ) |
2 |
|
simpl |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐻 Fn 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝐻 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝐻 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ) |
3 |
1
|
fpr1 |
⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝐹 Fn 𝐴 ) |
4 |
1
|
fpr2 |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) |
5 |
4
|
ralrimiva |
⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → ∀ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) |
6 |
3 5
|
jca |
⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝐹 Fn 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) |
7 |
6
|
adantr |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐻 Fn 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝐻 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝐻 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → ( 𝐹 Fn 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) |
8 |
|
simpr |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐻 Fn 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝐻 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝐻 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → ( 𝐻 Fn 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝐻 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝐻 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) |
9 |
|
fpr3g |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ∧ ( 𝐻 Fn 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝐻 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝐻 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → 𝐹 = 𝐻 ) |
10 |
2 7 8 9
|
syl3anc |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐻 Fn 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝐻 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝐻 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → 𝐹 = 𝐻 ) |