Theorem no3inds

Description: Triple induction over surreal numbers. The substitution instances cover all possible instances of less than or equal to x, y, and z. (Contributed by Scott Fenton, 21-Aug-2024)

	Ref	Expression
Hypotheses	no3inds.1	|- ( p = q -> ( ph <-> ps ) )
	no3inds.2	|- ( p = <. <. x , y >. , z >. -> ( ph <-> ch ) )
	no3inds.3	|- ( q = <. <. w , t >. , u >. -> ( ps <-> th ) )
	no3inds.4	|- ( u = z -> ( th <-> ta ) )
	no3inds.5	|- ( t = y -> ( th <-> et ) )
	no3inds.6	|- ( u = z -> ( et <-> ze ) )
	no3inds.7	|- ( w = x -> ( th <-> si ) )
	no3inds.8	|- ( u = z -> ( si <-> rh ) )
	no3inds.9	|- ( t = y -> ( si <-> mu ) )
	no3inds.10	|- ( x = A -> ( ch <-> la ) )
	no3inds.11	|- ( y = B -> ( la <-> ka ) )
	no3inds.12	|- ( z = C -> ( ka <-> al ) )
	no3inds.i	|- ( ( x e. No /\ y e. No /\ z e. No ) -> ( ( ( A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) th /\ A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( _L ` y ) u. ( _R ` y ) ) ta /\ A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) et ) /\ ( A. w e. ( ( _L ` x ) u. ( _R ` x ) ) ze /\ A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) si /\ A. t e. ( ( _L ` y ) u. ( _R ` y ) ) rh ) /\ A. u e. ( ( _L ` z ) u. ( _R ` z ) ) mu ) -> ch ) )
Assertion	no3inds	|- ( ( A e. No /\ B e. No /\ C e. No ) -> al )

Proof

Step	Hyp	Ref	Expression
1		no3inds.1	|- ( p = q -> ( ph <-> ps ) )
2		no3inds.2	|- ( p = <. <. x , y >. , z >. -> ( ph <-> ch ) )
3		no3inds.3	|- ( q = <. <. w , t >. , u >. -> ( ps <-> th ) )
4		no3inds.4	|- ( u = z -> ( th <-> ta ) )
5		no3inds.5	|- ( t = y -> ( th <-> et ) )
6		no3inds.6	|- ( u = z -> ( et <-> ze ) )
7		no3inds.7	|- ( w = x -> ( th <-> si ) )
8		no3inds.8	|- ( u = z -> ( si <-> rh ) )
9		no3inds.9	|- ( t = y -> ( si <-> mu ) )
10		no3inds.10	|- ( x = A -> ( ch <-> la ) )
11		no3inds.11	|- ( y = B -> ( la <-> ka ) )
12		no3inds.12	|- ( z = C -> ( ka <-> al ) )
13		no3inds.i	|- ( ( x e. No /\ y e. No /\ z e. No ) -> ( ( ( A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) th /\ A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( _L ` y ) u. ( _R ` y ) ) ta /\ A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) et ) /\ ( A. w e. ( ( _L ` x ) u. ( _R ` x ) ) ze /\ A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) si /\ A. t e. ( ( _L ` y ) u. ( _R ` y ) ) rh ) /\ A. u e. ( ( _L ` z ) u. ( _R ` z ) ) mu ) -> ch ) )
14		eqid	|- { <. a , b >. | a e. ( ( _L ` b ) u. ( _R ` b ) ) } = { <. a , b >. | a e. ( ( _L ` b ) u. ( _R ` b ) ) }
15		eqid	|- { <. c , d >. | ( c e. ( ( No X. No ) X. No ) /\ d e. ( ( No X. No ) X. No ) /\ ( ( ( ( 1st ` ( 1st ` c ) ) { <. a , b >. | a e. ( ( _L ` b ) u. ( _R ` b ) ) } ( 1st ` ( 1st ` d ) ) \/ ( 1st ` ( 1st ` c ) ) = ( 1st ` ( 1st ` d ) ) ) /\ ( ( 2nd ` ( 1st ` c ) ) { <. a , b >. | a e. ( ( _L ` b ) u. ( _R ` b ) ) } ( 2nd ` ( 1st ` d ) ) \/ ( 2nd ` ( 1st ` c ) ) = ( 2nd ` ( 1st ` d ) ) ) /\ ( ( 2nd ` c ) { <. a , b >. | a e. ( ( _L ` b ) u. ( _R ` b ) ) } ( 2nd ` d ) \/ ( 2nd ` c ) = ( 2nd ` d ) ) ) /\ c =/= d ) ) } = { <. c , d >. | ( c e. ( ( No X. No ) X. No ) /\ d e. ( ( No X. No ) X. No ) /\ ( ( ( ( 1st ` ( 1st ` c ) ) { <. a , b >. | a e. ( ( _L ` b ) u. ( _R ` b ) ) } ( 1st ` ( 1st ` d ) ) \/ ( 1st ` ( 1st ` c ) ) = ( 1st ` ( 1st ` d ) ) ) /\ ( ( 2nd ` ( 1st ` c ) ) { <. a , b >. | a e. ( ( _L ` b ) u. ( _R ` b ) ) } ( 2nd ` ( 1st ` d ) ) \/ ( 2nd ` ( 1st ` c ) ) = ( 2nd ` ( 1st ` d ) ) ) /\ ( ( 2nd ` c ) { <. a , b >. | a e. ( ( _L ` b ) u. ( _R ` b ) ) } ( 2nd ` d ) \/ ( 2nd ` c ) = ( 2nd ` d ) ) ) /\ c =/= d ) ) }
16	14 15 1 2 3 4 5 6 7 8 9 10 11 12 13	no3indslem	|- ( ( A e. No /\ B e. No /\ C e. No ) -> al )