Theorem no2indslem

Description: Double induction on surreals with explicit notation for the relationships. (Contributed by Scott Fenton, 22-Aug-2024)

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

Proof

Step	Hyp	Ref	Expression
1		no2indslem.a	Could not format R = { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } : No typesetting found for |- R = { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } with typecode |-
2		no2indslem.1	$$⊢x=z\to \left(\phi \leftrightarrow \psi \right)$$
3		no2indslem.2	$$⊢y=w\to \left(\psi \leftrightarrow \chi \right)$$
4		no2indslem.3	$$⊢x=z\to \left(\theta \leftrightarrow \chi \right)$$
5		no2indslem.4	$$⊢x=A\to \left(\phi \leftrightarrow \tau \right)$$
6		no2indslem.5	$$⊢y=B\to \left(\tau \leftrightarrow \eta \right)$$
7		no2indslem.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 |-
8	1	lrrecfr	$$⊢R\mathrm{Fr}\mathrm{No}$$
9	1	lrrecpo	$$⊢R\mathrm{Po}\mathrm{No}$$
10	1	lrrecse	$$⊢R\mathrm{Se}\mathrm{No}$$
11	1	lrrecpred	Could not format ( x e. No -> Pred ( R , No , x ) = ( ( _Left ` x ) u. ( _Right ` x ) ) ) : No typesetting found for |- ( x e. No -> Pred ( R , No , x ) = ( ( _Left ` x ) u. ( _Right ` x ) ) ) with typecode |-
12	11	adantr	Could not format ( ( x e. No /\ y e. No ) -> Pred ( R , No , x ) = ( ( _Left ` x ) u. ( _Right ` x ) ) ) : No typesetting found for |- ( ( x e. No /\ y e. No ) -> Pred ( R , No , x ) = ( ( _Left ` x ) u. ( _Right ` x ) ) ) with typecode |-
13	1	lrrecpred	Could not format ( y e. No -> Pred ( R , No , y ) = ( ( _Left ` y ) u. ( _Right ` y ) ) ) : No typesetting found for |- ( y e. No -> Pred ( R , No , y ) = ( ( _Left ` y ) u. ( _Right ` y ) ) ) with typecode |-
14	13	adantl	Could not format ( ( x e. No /\ y e. No ) -> Pred ( R , No , y ) = ( ( _Left ` y ) u. ( _Right ` y ) ) ) : No typesetting found for |- ( ( x e. No /\ y e. No ) -> Pred ( R , No , y ) = ( ( _Left ` y ) u. ( _Right ` y ) ) ) with typecode |-
15	14	raleqdv	Could not format ( ( x e. No /\ y e. No ) -> ( A. w e. Pred ( R , No , y ) ch <-> A. w e. ( ( _Left ` y ) u. ( _Right ` y ) ) ch ) ) : No typesetting found for |- ( ( x e. No /\ y e. No ) -> ( A. w e. Pred ( R , No , y ) ch <-> A. w e. ( ( _Left ` y ) u. ( _Right ` y ) ) ch ) ) with typecode |-
16	12 15	raleqbidv	Could not format ( ( x e. No /\ y e. No ) -> ( A. z e. Pred ( R , No , x ) A. w e. Pred ( R , No , y ) ch <-> A. z e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. w e. ( ( _Left ` y ) u. ( _Right ` y ) ) ch ) ) : No typesetting found for |- ( ( x e. No /\ y e. No ) -> ( A. z e. Pred ( R , No , x ) A. w e. Pred ( R , No , y ) ch <-> A. z e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. w e. ( ( _Left ` y ) u. ( _Right ` y ) ) ch ) ) with typecode |-
17	12	raleqdv	Could not format ( ( x e. No /\ y e. No ) -> ( A. z e. Pred ( R , No , x ) ps <-> A. z e. ( ( _Left ` x ) u. ( _Right ` x ) ) ps ) ) : No typesetting found for |- ( ( x e. No /\ y e. No ) -> ( A. z e. Pred ( R , No , x ) ps <-> A. z e. ( ( _Left ` x ) u. ( _Right ` x ) ) ps ) ) with typecode |-
18	14	raleqdv	Could not format ( ( x e. No /\ y e. No ) -> ( A. w e. Pred ( R , No , y ) th <-> A. w e. ( ( _Left ` y ) u. ( _Right ` y ) ) th ) ) : No typesetting found for |- ( ( x e. No /\ y e. No ) -> ( A. w e. Pred ( R , No , y ) th <-> A. w e. ( ( _Left ` y ) u. ( _Right ` y ) ) th ) ) with typecode |-
19	16 17 18	3anbi123d	Could not format ( ( x e. No /\ y e. No ) -> ( ( A. z e. Pred ( R , No , x ) A. w e. Pred ( R , No , y ) ch /\ A. z e. Pred ( R , No , x ) ps /\ A. w e. Pred ( R , No , y ) th ) <-> ( 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 ) ) ) : No typesetting found for |- ( ( x e. No /\ y e. No ) -> ( ( A. z e. Pred ( R , No , x ) A. w e. Pred ( R , No , y ) ch /\ A. z e. Pred ( R , No , x ) ps /\ A. w e. Pred ( R , No , y ) th ) <-> ( 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 ) ) ) with typecode |-
20	19 7	sylbid	$$⊢\left(x\in \mathrm{No}\wedge y\in \mathrm{No}\right)\to \left(\left(\forall z\in Pred\left(R,\mathrm{No},x\right)\forall w\in Pred\left(R,\mathrm{No},y\right)\chi \wedge \forall z\in Pred\left(R,\mathrm{No},x\right)\psi \wedge \forall w\in Pred\left(R,\mathrm{No},y\right)\theta \right)\to \phi \right)$$
21	8 9 10 8 9 10 2 3 4 5 6 20	xpord2ind	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \eta$$