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	⊢ 𝐹 = norec2 ( 𝐺 )
	Assertion	norec2ov	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 𝐹 𝐵 ) = ( ⟨ 𝐴 , 𝐵 ⟩ 𝐺 ( 𝐹 ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		norec2.1	⊢ 𝐹 = norec2 ( 𝐺 )
2		df-ov	⊢ ( 𝐴 𝐹 𝐵 ) = ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
3		opelxp	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( No × No ) ↔ ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) )
4		eqid	⊢ { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } = { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) }
5		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 ‘ 𝑏 ) ) ∧ 𝑎 ≠ 𝑏 ) ) }
6	4 5	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 )
7	4 5	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 )
8	4 5	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 )
9	6 7 8	3pm3.2i	⊢ ( { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ ( 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 ) )
10		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 ) , 𝐺 )
11	1 10	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 ) , 𝐺 )
12	11	fpr2	⊢ ( ( ( { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ ( 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 ) ) ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( No × No ) ) → ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ⟨ 𝐴 , 𝐵 ⟩ 𝐺 ( 𝐹 ↾ Pred ( { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ ( 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 ) , ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
13	9 12	mpan	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( No × No ) → ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ⟨ 𝐴 , 𝐵 ⟩ 𝐺 ( 𝐹 ↾ Pred ( { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ ( 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 ) , ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
14	3 13	sylbir	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ⟨ 𝐴 , 𝐵 ⟩ 𝐺 ( 𝐹 ↾ Pred ( { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ ( 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 ) , ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
15	2 14	syl5eq	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 𝐹 𝐵 ) = ( ⟨ 𝐴 , 𝐵 ⟩ 𝐺 ( 𝐹 ↾ Pred ( { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ ( 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 ) , ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
16	4 5	noxpordpred	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → Pred ( { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ ( 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 ) , ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
17	16	reseq2d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐹 ↾ Pred ( { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ ( 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 ) , ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( 𝐹 ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) )
18	17	oveq2d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ⟨ 𝐴 , 𝐵 ⟩ 𝐺 ( 𝐹 ↾ Pred ( { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ ( 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 ) , ⟨ 𝐴 , 𝐵 ⟩ ) ) ) = ( ⟨ 𝐴 , 𝐵 ⟩ 𝐺 ( 𝐹 ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ) )
19	15 18	eqtrd	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 𝐹 𝐵 ) = ( ⟨ 𝐴 , 𝐵 ⟩ 𝐺 ( 𝐹 ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ) )