Metamath Proof Explorer

Theorem norec2fn

Description: The double-recursion operator on surreals yields a function on pairs of surreals. (Contributed by Scott Fenton, 20-Aug-2024)

Ref Expression
Hypothesis norec2.1 ⊢ F = norec2 s #A# G
Assertion norec2fn ⊢ F Fn No × No

Proof

Step Hyp Ref Expression
1 norec2.1 ⊢ F = norec2 s #A# G
2 eqid ⊢ c d | c ∈ L ⁡ d ∪ R ⁡ d = c d | c ∈ L ⁡ d ∪ R ⁡ d
3 eqid ⊢ a b | a ∈ No × No ∧ b ∈ No × No ∧ 1 st ⁡ a c d | c ∈ L ⁡ d ∪ R ⁡ d 1 st ⁡ b ∨ 1 st ⁡ a = 1 st ⁡ b ∧ 2 nd ⁡ a c d | c ∈ L ⁡ d ∪ R ⁡ d 2 nd ⁡ b ∨ 2 nd ⁡ a = 2 nd ⁡ b ∧ a ≠ b = a b | a ∈ No × No ∧ b ∈ No × No ∧ 1 st ⁡ a c d | c ∈ L ⁡ d ∪ R ⁡ d 1 st ⁡ b ∨ 1 st ⁡ a = 1 st ⁡ b ∧ 2 nd ⁡ a c d | c ∈ L ⁡ d ∪ R ⁡ d 2 nd ⁡ b ∨ 2 nd ⁡ a = 2 nd ⁡ b ∧ a ≠ b
4 2 3 noxpordfr ⊢ a b | a ∈ No × No ∧ b ∈ No × No ∧ 1 st ⁡ a c d | c ∈ L ⁡ d ∪ R ⁡ d 1 st ⁡ b ∨ 1 st ⁡ a = 1 st ⁡ b ∧ 2 nd ⁡ a c d | c ∈ L ⁡ d ∪ R ⁡ d 2 nd ⁡ b ∨ 2 nd ⁡ a = 2 nd ⁡ b ∧ a ≠ b Fr No × No
5 2 3 noxpordpo ⊢ a b | a ∈ No × No ∧ b ∈ No × No ∧ 1 st ⁡ a c d | c ∈ L ⁡ d ∪ R ⁡ d 1 st ⁡ b ∨ 1 st ⁡ a = 1 st ⁡ b ∧ 2 nd ⁡ a c d | c ∈ L ⁡ d ∪ R ⁡ d 2 nd ⁡ b ∨ 2 nd ⁡ a = 2 nd ⁡ b ∧ a ≠ b Po No × No
6 2 3 noxpordse ⊢ a b | a ∈ No × No ∧ b ∈ No × No ∧ 1 st ⁡ a c d | c ∈ L ⁡ d ∪ R ⁡ d 1 st ⁡ b ∨ 1 st ⁡ a = 1 st ⁡ b ∧ 2 nd ⁡ a c d | c ∈ L ⁡ d ∪ R ⁡ d 2 nd ⁡ b ∨ 2 nd ⁡ a = 2 nd ⁡ b ∧ a ≠ b Se No × No
7 df-norec2 ⊢ norec2 s #A# G = frecs ⁡ a b | a ∈ No × No ∧ b ∈ No × No ∧ 1 st ⁡ a c d | c ∈ L ⁡ d ∪ R ⁡ d 1 st ⁡ b ∨ 1 st ⁡ a = 1 st ⁡ b ∧ 2 nd ⁡ a c d | c ∈ L ⁡ d ∪ R ⁡ d 2 nd ⁡ b ∨ 2 nd ⁡ a = 2 nd ⁡ b ∧ a ≠ b No × No G
8 1 7 eqtri ⊢ F = frecs ⁡ a b | a ∈ No × No ∧ b ∈ No × No ∧ 1 st ⁡ a c d | c ∈ L ⁡ d ∪ R ⁡ d 1 st ⁡ b ∨ 1 st ⁡ a = 1 st ⁡ b ∧ 2 nd ⁡ a c d | c ∈ L ⁡ d ∪ R ⁡ d 2 nd ⁡ b ∨ 2 nd ⁡ a = 2 nd ⁡ b ∧ a ≠ b No × No G
9 8 fpr1 ⊢ a b | a ∈ No × No ∧ b ∈ No × No ∧ 1 st ⁡ a c d | c ∈ L ⁡ d ∪ R ⁡ d 1 st ⁡ b ∨ 1 st ⁡ a = 1 st ⁡ b ∧ 2 nd ⁡ a c d | c ∈ L ⁡ d ∪ R ⁡ d 2 nd ⁡ b ∨ 2 nd ⁡ a = 2 nd ⁡ b ∧ a ≠ b Fr No × No ∧ a b | a ∈ No × No ∧ b ∈ No × No ∧ 1 st ⁡ a c d | c ∈ L ⁡ d ∪ R ⁡ d 1 st ⁡ b ∨ 1 st ⁡ a = 1 st ⁡ b ∧ 2 nd ⁡ a c d | c ∈ L ⁡ d ∪ R ⁡ d 2 nd ⁡ b ∨ 2 nd ⁡ a = 2 nd ⁡ b ∧ a ≠ b Po No × No ∧ a b | a ∈ No × No ∧ b ∈ No × No ∧ 1 st ⁡ a c d | c ∈ L ⁡ d ∪ R ⁡ d 1 st ⁡ b ∨ 1 st ⁡ a = 1 st ⁡ b ∧ 2 nd ⁡ a c d | c ∈ L ⁡ d ∪ R ⁡ d 2 nd ⁡ b ∨ 2 nd ⁡ a = 2 nd ⁡ b ∧ a ≠ b Se No × No → F Fn No × No
10 4 5 6 9 mp3an ⊢ F Fn No × No