Metamath Proof Explorer

Theorem wfr3

Description: The principle of Well-Ordered Recursion, part 3 of 3. Finally, we show that F is unique. We do this by showing that any function H with the same properties we proved of F in wfr1 and wfr2 is identical to F . (Contributed by Scott Fenton, 18-Apr-2011) (Revised by Mario Carneiro, 26-Jun-2015) (Revised by Scott Fenton, 18-Nov-2024)

Ref Expression
Hypothesis wfr3.3 ⊢ F = wrecs ⁡ R A G
Assertion wfr3 ⊢ R We A ∧ R Se A ∧ H Fn A ∧ ∀ z ∈ A H ⁡ z = G ⁡ H ↾ Pred R A z → F = H

Proof

Step Hyp Ref Expression
1 wfr3.3 ⊢ F = wrecs ⁡ R A G
2 simpl ⊢ R We A ∧ R Se A ∧ H Fn A ∧ ∀ z ∈ A H ⁡ z = G ⁡ H ↾ Pred R A z → R We A ∧ R Se A
3 1 wfr1 ⊢ R We A ∧ R Se A → F Fn A
4 1 wfr2 ⊢ R We A ∧ R Se A ∧ z ∈ A → F ⁡ z = G ⁡ F ↾ Pred R A z
5 4 ralrimiva ⊢ R We A ∧ R Se A → ∀ z ∈ A F ⁡ z = G ⁡ F ↾ Pred R A z
6 3 5 jca ⊢ R We A ∧ R Se A → F Fn A ∧ ∀ z ∈ A F ⁡ z = G ⁡ F ↾ Pred R A z
7 6 adantr ⊢ R We A ∧ R Se A ∧ H Fn A ∧ ∀ z ∈ A H ⁡ z = G ⁡ H ↾ Pred R A z → F Fn A ∧ ∀ z ∈ A F ⁡ z = G ⁡ F ↾ Pred R A z
8 simpr ⊢ R We A ∧ R Se A ∧ H Fn A ∧ ∀ z ∈ A H ⁡ z = G ⁡ H ↾ Pred R A z → H Fn A ∧ ∀ z ∈ A H ⁡ z = G ⁡ H ↾ Pred R A z
9 wfr3g ⊢ R We A ∧ R Se A ∧ F Fn A ∧ ∀ z ∈ A F ⁡ z = G ⁡ F ↾ Pred R A z ∧ H Fn A ∧ ∀ z ∈ A H ⁡ z = G ⁡ H ↾ Pred R A z → F = H
10 2 7 8 9 syl3anc ⊢ R We A ∧ R Se A ∧ H Fn A ∧ ∀ z ∈ A H ⁡ z = G ⁡ H ↾ Pred R A z → F = H