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\to \left(\phi \leftrightarrow \psi \right)$$
	no2inds.2	$$⊢y=w\to \left(\psi \leftrightarrow \chi \right)$$
	no2inds.3	$$⊢x=z\to \left(\theta \leftrightarrow \chi \right)$$
	no2inds.4	$$⊢x=A\to \left(\phi \leftrightarrow \tau \right)$$
	no2inds.5	$$⊢y=B\to \left(\tau \leftrightarrow \eta \right)$$
	no2inds.i	No typesetting found for |- ( ( 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 ) ) with typecode |-
Assertion	no2inds	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \eta$$

Proof

Step	Hyp	Ref	Expression
1		no2inds.1	$$⊢x=z\to \left(\phi \leftrightarrow \psi \right)$$
2		no2inds.2	$$⊢y=w\to \left(\psi \leftrightarrow \chi \right)$$
3		no2inds.3	$$⊢x=z\to \left(\theta \leftrightarrow \chi \right)$$
4		no2inds.4	$$⊢x=A\to \left(\phi \leftrightarrow \tau \right)$$
5		no2inds.5	$$⊢y=B\to \left(\tau \leftrightarrow \eta \right)$$
6		no2inds.i	Could not format ( ( 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 ) ) : No typesetting found for |- ( ( 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 ) ) with typecode |-
7		eqid	Could not format { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } = { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } : No typesetting found for |- { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } = { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } with typecode |-
8	7 1 2 3 4 5 6	no2indslem	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \eta$$