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	Could not format assertion : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( A F B ) = ( <. A , B >. G ( F |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ) ) with typecode |-

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	$$⊢AFB=F\left(⟨A,B⟩\right)$$
3		opelxp	$$⊢⟨A,B⟩\in \left(\mathrm{No}\times \mathrm{No}\right)\leftrightarrow \left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)$$
4		eqid	Could not format { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } = { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } : No typesetting found for |- { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } = { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } with typecode |-
5		eqid	Could not format { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } = { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } : No typesetting found for |- { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } = { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } with typecode |-
6	4 5	noxpordfr	Could not format { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } Fr ( No X. No ) : No typesetting found for |- { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } Fr ( No X. No ) with typecode |-
7	4 5	noxpordpo	Could not format { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } Po ( No X. No ) : No typesetting found for |- { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } Po ( No X. No ) with typecode |-
8	4 5	noxpordse	Could not format { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } Se ( No X. No ) : No typesetting found for |- { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } Se ( No X. No ) with typecode |-
9	6 7 8	3pm3.2i	Could not format ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } Fr ( No X. No ) /\ { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } Po ( No X. No ) /\ { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } Se ( No X. No ) ) : No typesetting found for |- ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } Fr ( No X. No ) /\ { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } Po ( No X. No ) /\ { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } Se ( No X. No ) ) with typecode |-
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. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` 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. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , G ) with typecode |-
11	1 10	eqtri	Could not format F = frecs ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , G ) : No typesetting found for |- F = frecs ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , G ) with typecode |-
12	11	fpr2	Could not format ( ( ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } Fr ( No X. No ) /\ { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } Po ( No X. No ) /\ { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } Se ( No X. No ) ) /\ <. A , B >. e. ( No X. No ) ) -> ( F ` <. A , B >. ) = ( <. A , B >. G ( F |` Pred ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , <. A , B >. ) ) ) ) : No typesetting found for |- ( ( ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } Fr ( No X. No ) /\ { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } Po ( No X. No ) /\ { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } Se ( No X. No ) ) /\ <. A , B >. e. ( No X. No ) ) -> ( F ` <. A , B >. ) = ( <. A , B >. G ( F |` Pred ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , <. A , B >. ) ) ) ) with typecode |-
13	9 12	mpan	Could not format ( <. A , B >. e. ( No X. No ) -> ( F ` <. A , B >. ) = ( <. A , B >. G ( F |` Pred ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , <. A , B >. ) ) ) ) : No typesetting found for |- ( <. A , B >. e. ( No X. No ) -> ( F ` <. A , B >. ) = ( <. A , B >. G ( F |` Pred ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , <. A , B >. ) ) ) ) with typecode |-
14	3 13	sylbir	Could not format ( ( A e. No /\ B e. No ) -> ( F ` <. A , B >. ) = ( <. A , B >. G ( F |` Pred ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , <. A , B >. ) ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( F ` <. A , B >. ) = ( <. A , B >. G ( F |` Pred ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , <. A , B >. ) ) ) ) with typecode |-
15	2 14	eqtrid	Could not format ( ( A e. No /\ B e. No ) -> ( A F B ) = ( <. A , B >. G ( F |` Pred ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , <. A , B >. ) ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( A F B ) = ( <. A , B >. G ( F |` Pred ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , <. A , B >. ) ) ) ) with typecode |-
16	4 5	noxpordpred	Could not format ( ( A e. No /\ B e. No ) -> Pred ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , <. A , B >. ) = ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> Pred ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , <. A , B >. ) = ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) with typecode |-
17	16	reseq2d	Could not format ( ( A e. No /\ B e. No ) -> ( F |` Pred ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , <. A , B >. ) ) = ( F |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( F |` Pred ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , <. A , B >. ) ) = ( F |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ) with typecode |-
18	17	oveq2d	Could not format ( ( A e. No /\ B e. No ) -> ( <. A , B >. G ( F |` Pred ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , <. A , B >. ) ) ) = ( <. A , B >. G ( F |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( <. A , B >. G ( F |` Pred ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , <. A , B >. ) ) ) = ( <. A , B >. G ( F |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ) ) with typecode |-
19	15 18	eqtrd	Could not format ( ( A e. No /\ B e. No ) -> ( A F B ) = ( <. A , B >. G ( F |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( A F B ) = ( <. A , B >. G ( F |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ) ) with typecode |-