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	No typesetting found for |- F = norec2 ( G ) with typecode |-
Assertion	norec2fn	$$⊢FFn\left(\mathrm{No}\times \mathrm{No}\right)$$

Proof

Step	Hyp	Ref	Expression
1		norec2.1	Could not format F = norec2 ( G ) : No typesetting found for |- F = norec2 ( G ) with typecode |-
2		eqid	$$⊢\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}=\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}$$
3		eqid	$$⊢\left\{⟨a,b⟩|\left(a\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge b\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge \left(\left(1^{st}\left(a\right)\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}{1}^{st}\left(b\right)\vee 1^{st}\left(a\right)=1^{st}\left(b\right)\right)\wedge \left(2^{nd}\left(a\right)\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}{2}^{nd}\left(b\right)\vee 2^{nd}\left(a\right)=2^{nd}\left(b\right)\right)\wedge a\ne b\right)\right)\right\}=\left\{⟨a,b⟩|\left(a\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge b\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge \left(\left(1^{st}\left(a\right)\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}{1}^{st}\left(b\right)\vee 1^{st}\left(a\right)=1^{st}\left(b\right)\right)\wedge \left(2^{nd}\left(a\right)\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}{2}^{nd}\left(b\right)\vee 2^{nd}\left(a\right)=2^{nd}\left(b\right)\right)\wedge a\ne b\right)\right)\right\}$$
4	2 3	noxpordfr	$$⊢\left\{⟨a,b⟩|\left(a\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge b\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge \left(\left(1^{st}\left(a\right)\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}{1}^{st}\left(b\right)\vee 1^{st}\left(a\right)=1^{st}\left(b\right)\right)\wedge \left(2^{nd}\left(a\right)\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}{2}^{nd}\left(b\right)\vee 2^{nd}\left(a\right)=2^{nd}\left(b\right)\right)\wedge a\ne b\right)\right)\right\}\mathrm{Fr}\left(\mathrm{No}\times \mathrm{No}\right)$$
5	2 3	noxpordpo	$$⊢\left\{⟨a,b⟩|\left(a\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge b\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge \left(\left(1^{st}\left(a\right)\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}{1}^{st}\left(b\right)\vee 1^{st}\left(a\right)=1^{st}\left(b\right)\right)\wedge \left(2^{nd}\left(a\right)\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}{2}^{nd}\left(b\right)\vee 2^{nd}\left(a\right)=2^{nd}\left(b\right)\right)\wedge a\ne b\right)\right)\right\}\mathrm{Po}\left(\mathrm{No}\times \mathrm{No}\right)$$
6	2 3	noxpordse	$$⊢\left\{⟨a,b⟩|\left(a\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge b\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge \left(\left(1^{st}\left(a\right)\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}{1}^{st}\left(b\right)\vee 1^{st}\left(a\right)=1^{st}\left(b\right)\right)\wedge \left(2^{nd}\left(a\right)\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}{2}^{nd}\left(b\right)\vee 2^{nd}\left(a\right)=2^{nd}\left(b\right)\right)\wedge a\ne b\right)\right)\right\}\mathrm{Se}\left(\mathrm{No}\times \mathrm{No}\right)$$
7		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 |-
8	1 7	eqtri	$$⊢F=\mathrm{frecs}\left(\left\{⟨a,b⟩|\left(a\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge b\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge \left(\left(1^{st}\left(a\right)\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}{1}^{st}\left(b\right)\vee 1^{st}\left(a\right)=1^{st}\left(b\right)\right)\wedge \left(2^{nd}\left(a\right)\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}{2}^{nd}\left(b\right)\vee 2^{nd}\left(a\right)=2^{nd}\left(b\right)\right)\wedge a\ne b\right)\right)\right\},\mathrm{No}\times \mathrm{No},G\right)$$
9	8	fpr1	$$⊢\left(\left\{⟨a,b⟩|\left(a\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge b\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge \left(\left(1^{st}\left(a\right)\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}{1}^{st}\left(b\right)\vee 1^{st}\left(a\right)=1^{st}\left(b\right)\right)\wedge \left(2^{nd}\left(a\right)\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}{2}^{nd}\left(b\right)\vee 2^{nd}\left(a\right)=2^{nd}\left(b\right)\right)\wedge a\ne b\right)\right)\right\}\mathrm{Fr}\left(\mathrm{No}\times \mathrm{No}\right)\wedge \left\{⟨a,b⟩|\left(a\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge b\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge \left(\left(1^{st}\left(a\right)\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}{1}^{st}\left(b\right)\vee 1^{st}\left(a\right)=1^{st}\left(b\right)\right)\wedge \left(2^{nd}\left(a\right)\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}{2}^{nd}\left(b\right)\vee 2^{nd}\left(a\right)=2^{nd}\left(b\right)\right)\wedge a\ne b\right)\right)\right\}\mathrm{Po}\left(\mathrm{No}\times \mathrm{No}\right)\wedge \left\{⟨a,b⟩|\left(a\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge b\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge \left(\left(1^{st}\left(a\right)\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}{1}^{st}\left(b\right)\vee 1^{st}\left(a\right)=1^{st}\left(b\right)\right)\wedge \left(2^{nd}\left(a\right)\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}{2}^{nd}\left(b\right)\vee 2^{nd}\left(a\right)=2^{nd}\left(b\right)\right)\wedge a\ne b\right)\right)\right\}\mathrm{Se}\left(\mathrm{No}\times \mathrm{No}\right)\right)\to FFn\left(\mathrm{No}\times \mathrm{No}\right)$$
10	4 5 6 9	mp3an	$$⊢FFn\left(\mathrm{No}\times \mathrm{No}\right)$$