Theorem no2inds

Description: Double induction on surreals. The many substitution instances are to cover all possible cases. (Contributed by Scott Fenton, 22-Aug-2024)

	Ref	Expression
Hypotheses	no2inds.1	|- ( x = z -> ( ph <-> ps ) )
	no2inds.2	|- ( y = w -> ( ps <-> ch ) )
	no2inds.3	|- ( x = z -> ( th <-> ch ) )
	no2inds.4	|- ( x = A -> ( ph <-> ta ) )
	no2inds.5	|- ( y = B -> ( ta <-> et ) )
	no2inds.i	|- ( ( x e. No /\ y e. No ) -> ( ( A. z e. ( ( _L ` x ) u. ( _R ` x ) ) A. w e. ( ( _L ` y ) u. ( _R ` y ) ) ch /\ A. z e. ( ( _L ` x ) u. ( _R ` x ) ) ps /\ A. w e. ( ( _L ` y ) u. ( _R ` y ) ) th ) -> ph ) )
Assertion	no2inds	|- ( ( A e. No /\ B e. No ) -> et )

Proof

Step	Hyp	Ref	Expression
1		no2inds.1	|- ( x = z -> ( ph <-> ps ) )
2		no2inds.2	|- ( y = w -> ( ps <-> ch ) )
3		no2inds.3	|- ( x = z -> ( th <-> ch ) )
4		no2inds.4	|- ( x = A -> ( ph <-> ta ) )
5		no2inds.5	|- ( y = B -> ( ta <-> et ) )
6		no2inds.i	|- ( ( x e. No /\ y e. No ) -> ( ( A. z e. ( ( _L ` x ) u. ( _R ` x ) ) A. w e. ( ( _L ` y ) u. ( _R ` y ) ) ch /\ A. z e. ( ( _L ` x ) u. ( _R ` x ) ) ps /\ A. w e. ( ( _L ` y ) u. ( _R ` y ) ) th ) -> ph ) )
7		eqid	|- { <. a , b >. | a e. ( ( _L ` b ) u. ( _R ` b ) ) } = { <. a , b >. | a e. ( ( _L ` b ) u. ( _R ` b ) ) }
8		eqid	|- { <. c , d >. | ( c e. ( No X. No ) /\ d e. ( No X. No ) /\ ( ( ( 1st ` c ) { <. a , b >. | a e. ( ( _L ` b ) u. ( _R ` b ) ) } ( 1st ` d ) \/ ( 1st ` c ) = ( 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 ) /\ d e. ( No X. No ) /\ ( ( ( 1st ` c ) { <. a , b >. | a e. ( ( _L ` b ) u. ( _R ` b ) ) } ( 1st ` d ) \/ ( 1st ` c ) = ( 1st ` d ) ) /\ ( ( 2nd ` c ) { <. a , b >. | a e. ( ( _L ` b ) u. ( _R ` b ) ) } ( 2nd ` d ) \/ ( 2nd ` c ) = ( 2nd ` d ) ) /\ c =/= d ) ) }
9	7 8 1 2 3 4 5 6	no2indslem	|- ( ( A e. No /\ B e. No ) -> et )