Description: The Principle of Well-Ordered Recursion, part 2 of 3. Next, we show that the value of F at any X e. A is G applied to all "previous" values of F . (Contributed by Scott Fenton, 18-Apr-2011) (Revised by Mario Carneiro, 26-Jun-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | wfr2.1 | ⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 ) | |
| Assertion | wfr2 | ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wfr2.1 | ⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 ) | |
| 2 | 1 | wfr1 | ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝐹 Fn 𝐴 ) |
| 3 | 2 | fndmd | ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → dom 𝐹 = 𝐴 ) |
| 4 | 3 | eleq2d | ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑋 ∈ dom 𝐹 ↔ 𝑋 ∈ 𝐴 ) ) |
| 5 | 4 | biimpar | ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ dom 𝐹 ) |
| 6 | 1 | wfr2a | ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) ) |
| 7 | 5 6 | syldan | ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) ) |