Metamath Proof Explorer

Theorem wfr3

Description: The principle of Well-Founded 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)

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

Proof

Step Hyp Ref Expression
1 wfr3.1 ⊢ R We A
2 wfr3.2 ⊢ R Se A
3 wfr3.3 ⊢ F = wrecs ⁡ R A G
4 1 2 pm3.2i ⊢ R We A ∧ R Se A
5 1 2 3 wfr1 ⊢ F Fn A
6 1 2 3 wfr2 ⊢ z ∈ A → F ⁡ z = G ⁡ F ↾ Pred R A z
7 6 rgen ⊢ ∀ z ∈ A F ⁡ z = G ⁡ F ↾ Pred R A z
8 5 7 pm3.2i ⊢ F Fn A ∧ ∀ z ∈ A F ⁡ z = G ⁡ F ↾ 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 4 8 9 mp3an12 ⊢ H Fn A ∧ ∀ z ∈ A H ⁡ z = G ⁡ H ↾ Pred R A z → F = H