Metamath Proof Explorer

Theorem norec2ov

Description: The value of the double-recursion surreal function. (Contributed by Scott Fenton, 20-Aug-2024)

Ref Expression
Hypothesis norec2.1 No typesetting found for |- F = norec2 ( G ) with typecode |-
Assertion norec2ov ⊢ A ∈ No ∧ B ∈ No → A F B = A B G F ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B

Proof

Step Hyp Ref Expression
1 norec2.1 Could not format F = norec2 ( G ) : No typesetting found for |- F = norec2 ( G ) with typecode |-
2 df-ov ⊢ A F B = F ⁡ A B
3 opelxp ⊢ A B ∈ No × No ↔ A ∈ No ∧ B ∈ No
4 eqid ⊢ c d | c ∈ L ⁡ d ∪ R ⁡ d = c d | c ∈ L ⁡ d ∪ R ⁡ d
5 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
6 4 5 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
7 4 5 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
8 4 5 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
9 6 7 8 3pm3.2i ⊢ 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
10 df-norec2 Could not format norec2 ( G ) = frecs ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _L ` d ) u. ( _R ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _L ` d ) u. ( _R ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , G ) : No typesetting found for |- norec2 ( G ) = frecs ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _L ` d ) u. ( _R ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _L ` d ) u. ( _R ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , G ) with typecode |-
11 1 10 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
12 11 fpr2 ⊢ 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 ∧ A B ∈ No × No → F ⁡ A B = A B G F ↾ Pred 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 A B
13 9 12 mpan ⊢ A B ∈ No × No → F ⁡ A B = A B G F ↾ Pred 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 A B
14 3 13 sylbir ⊢ A ∈ No ∧ B ∈ No → F ⁡ A B = A B G F ↾ Pred 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 A B
15 2 14 syl5eq ⊢ A ∈ No ∧ B ∈ No → A F B = A B G F ↾ Pred 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 A B
16 4 5 noxpordpred ⊢ A ∈ No ∧ B ∈ No → Pred 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 A B = L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B
17 16 reseq2d ⊢ A ∈ No ∧ B ∈ No → F ↾ Pred 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 A B = F ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B
18 17 oveq2d ⊢ A ∈ No ∧ B ∈ No → A B G F ↾ Pred 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 A B = A B G F ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B
19 15 18 eqtrd ⊢ A ∈ No ∧ B ∈ No → A F B = A B G F ↾ L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B