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	⊢ 𝐹 = norec2 ( 𝐺 )
	Assertion	norec2fn	⊢ 𝐹 Fn ( No × No )

Proof

Step	Hyp	Ref	Expression
1		norec2.1	⊢ 𝐹 = norec2 ( 𝐺 )
2		eqid	⊢ { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } = { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) }
3		eqid	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ ( ( ( 1^st ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 1^st ‘ 𝑏 ) ∨ ( 1^st ‘ 𝑎 ) = ( 1^st ‘ 𝑏 ) ) ∧ ( ( 2^nd ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 2^nd ‘ 𝑏 ) ∨ ( 2^nd ‘ 𝑎 ) = ( 2^nd ‘ 𝑏 ) ) ∧ 𝑎 ≠ 𝑏 ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ ( ( ( 1^st ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 1^st ‘ 𝑏 ) ∨ ( 1^st ‘ 𝑎 ) = ( 1^st ‘ 𝑏 ) ) ∧ ( ( 2^nd ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 2^nd ‘ 𝑏 ) ∨ ( 2^nd ‘ 𝑎 ) = ( 2^nd ‘ 𝑏 ) ) ∧ 𝑎 ≠ 𝑏 ) ) }
4	2 3	noxpordfr	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ ( ( ( 1^st ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 1^st ‘ 𝑏 ) ∨ ( 1^st ‘ 𝑎 ) = ( 1^st ‘ 𝑏 ) ) ∧ ( ( 2^nd ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 2^nd ‘ 𝑏 ) ∨ ( 2^nd ‘ 𝑎 ) = ( 2^nd ‘ 𝑏 ) ) ∧ 𝑎 ≠ 𝑏 ) ) } Fr ( No × No )
5	2 3	noxpordpo	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ ( ( ( 1^st ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 1^st ‘ 𝑏 ) ∨ ( 1^st ‘ 𝑎 ) = ( 1^st ‘ 𝑏 ) ) ∧ ( ( 2^nd ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 2^nd ‘ 𝑏 ) ∨ ( 2^nd ‘ 𝑎 ) = ( 2^nd ‘ 𝑏 ) ) ∧ 𝑎 ≠ 𝑏 ) ) } Po ( No × No )
6	2 3	noxpordse	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ ( ( ( 1^st ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 1^st ‘ 𝑏 ) ∨ ( 1^st ‘ 𝑎 ) = ( 1^st ‘ 𝑏 ) ) ∧ ( ( 2^nd ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 2^nd ‘ 𝑏 ) ∨ ( 2^nd ‘ 𝑎 ) = ( 2^nd ‘ 𝑏 ) ) ∧ 𝑎 ≠ 𝑏 ) ) } Se ( No × No )
7		df-norec2	⊢ norec2 ( 𝐺 ) = frecs ( { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ ( ( ( 1^st ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 1^st ‘ 𝑏 ) ∨ ( 1^st ‘ 𝑎 ) = ( 1^st ‘ 𝑏 ) ) ∧ ( ( 2^nd ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 2^nd ‘ 𝑏 ) ∨ ( 2^nd ‘ 𝑎 ) = ( 2^nd ‘ 𝑏 ) ) ∧ 𝑎 ≠ 𝑏 ) ) } , ( No × No ) , 𝐺 )
8	1 7	eqtri	⊢ 𝐹 = frecs ( { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ ( ( ( 1^st ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 1^st ‘ 𝑏 ) ∨ ( 1^st ‘ 𝑎 ) = ( 1^st ‘ 𝑏 ) ) ∧ ( ( 2^nd ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 2^nd ‘ 𝑏 ) ∨ ( 2^nd ‘ 𝑎 ) = ( 2^nd ‘ 𝑏 ) ) ∧ 𝑎 ≠ 𝑏 ) ) } , ( No × No ) , 𝐺 )
9	8	fpr1	⊢ ( ( { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ ( ( ( 1^st ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 1^st ‘ 𝑏 ) ∨ ( 1^st ‘ 𝑎 ) = ( 1^st ‘ 𝑏 ) ) ∧ ( ( 2^nd ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 2^nd ‘ 𝑏 ) ∨ ( 2^nd ‘ 𝑎 ) = ( 2^nd ‘ 𝑏 ) ) ∧ 𝑎 ≠ 𝑏 ) ) } Fr ( No × No ) ∧ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ ( ( ( 1^st ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 1^st ‘ 𝑏 ) ∨ ( 1^st ‘ 𝑎 ) = ( 1^st ‘ 𝑏 ) ) ∧ ( ( 2^nd ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 2^nd ‘ 𝑏 ) ∨ ( 2^nd ‘ 𝑎 ) = ( 2^nd ‘ 𝑏 ) ) ∧ 𝑎 ≠ 𝑏 ) ) } Po ( No × No ) ∧ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ ( ( ( 1^st ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 1^st ‘ 𝑏 ) ∨ ( 1^st ‘ 𝑎 ) = ( 1^st ‘ 𝑏 ) ) ∧ ( ( 2^nd ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 2^nd ‘ 𝑏 ) ∨ ( 2^nd ‘ 𝑎 ) = ( 2^nd ‘ 𝑏 ) ) ∧ 𝑎 ≠ 𝑏 ) ) } Se ( No × No ) ) → 𝐹 Fn ( No × No ) )
10	4 5 6 9	mp3an	⊢ 𝐹 Fn ( No × No )