Metamath Proof Explorer

Theorem norecov

Description: Calculate the value of the surreal recursion operation. (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Hypothesis norec.1 ⊢ F = norec s #A# G
Assertion norecov ⊢ A ∈ No → F ⁡ A = A G F ↾ L ⁡ A ∪ R ⁡ A

Proof

Step Hyp Ref Expression
1 norec.1 ⊢ F = norec s #A# G
2 eqid ⊢ x y | x ∈ L ⁡ y ∪ R ⁡ y = x y | x ∈ L ⁡ y ∪ R ⁡ y
3 2 lrrecfr ⊢ x y | x ∈ L ⁡ y ∪ R ⁡ y Fr No
4 2 lrrecpo ⊢ x y | x ∈ L ⁡ y ∪ R ⁡ y Po No
5 2 lrrecse ⊢ x y | x ∈ L ⁡ y ∪ R ⁡ y Se No
6 3 4 5 3pm3.2i ⊢ x y | x ∈ L ⁡ y ∪ R ⁡ y Fr No ∧ x y | x ∈ L ⁡ y ∪ R ⁡ y Po No ∧ x y | x ∈ L ⁡ y ∪ R ⁡ y Se No
7 df-norec ⊢ norec s #A# G = frecs ⁡ x y | x ∈ L ⁡ y ∪ R ⁡ y No G
8 1 7 eqtri ⊢ F = frecs ⁡ x y | x ∈ L ⁡ y ∪ R ⁡ y No G
9 8 fpr2 ⊢ x y | x ∈ L ⁡ y ∪ R ⁡ y Fr No ∧ x y | x ∈ L ⁡ y ∪ R ⁡ y Po No ∧ x y | x ∈ L ⁡ y ∪ R ⁡ y Se No ∧ A ∈ No → F ⁡ A = A G F ↾ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No A
10 6 9 mpan ⊢ A ∈ No → F ⁡ A = A G F ↾ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No A
11 2 lrrecpred ⊢ A ∈ No → Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No A = L ⁡ A ∪ R ⁡ A
12 11 reseq2d ⊢ A ∈ No → F ↾ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No A = F ↾ L ⁡ A ∪ R ⁡ A
13 12 oveq2d ⊢ A ∈ No → A G F ↾ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No A = A G F ↾ L ⁡ A ∪ R ⁡ A
14 10 13 eqtrd ⊢ A ∈ No → F ⁡ A = A G F ↾ L ⁡ A ∪ R ⁡ A