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. ( ( _Left ` x ) u. ( _Right ` x ) ) A. w e. ( ( _Left ` y ) u. ( _Right ` y ) ) ch /\ A. z e. ( ( _Left ` x ) u. ( _Right ` x ) ) ps /\ A. w e. ( ( _Left ` y ) u. ( _Right ` 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. ( ( _Left ` x ) u. ( _Right ` x ) ) A. w e. ( ( _Left ` y ) u. ( _Right ` y ) ) ch /\ A. z e. ( ( _Left ` x ) u. ( _Right ` x ) ) ps /\ A. w e. ( ( _Left ` y ) u. ( _Right ` y ) ) th ) -> ph ) )
7		eqid	|- { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } = { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) }
8	7 1 2 3 4 5 6	no2indslem	|- ( ( A e. No /\ B e. No ) -> et )