Theorem noinds

Description: Induction principle for a single surreal. If a property passes from a surreal's left and right sets to the surreal itself, then it holds for all surreals. (Contributed by Scott Fenton, 19-Aug-2024)

	Ref	Expression
Hypotheses	noinds.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
	noinds.2	$$⊢x=A\to \left(\phi \leftrightarrow \chi \right)$$
	noinds.3	No typesetting found for |- ( x e. No -> ( A. y e. ( ( _Left ` x ) u. ( _Right ` x ) ) ps -> ph ) ) with typecode |-
Assertion	noinds	$$⊢A\in \mathrm{No}\to \chi$$

Proof

Step	Hyp	Ref	Expression
1		noinds.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
2		noinds.2	$$⊢x=A\to \left(\phi \leftrightarrow \chi \right)$$
3		noinds.3	Could not format ( x e. No -> ( A. y e. ( ( _Left ` x ) u. ( _Right ` x ) ) ps -> ph ) ) : No typesetting found for |- ( x e. No -> ( A. y e. ( ( _Left ` x ) u. ( _Right ` x ) ) ps -> ph ) ) with typecode |-
4		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 |-
5	4	lrrecfr	Could not format { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } Fr No : No typesetting found for |- { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } Fr No with typecode |-
6	4	lrrecpo	Could not format { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } Po No : No typesetting found for |- { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } Po No with typecode |-
7	4	lrrecse	Could not format { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } Se No : No typesetting found for |- { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } Se No with typecode |-
8	5 6 7	3pm3.2i	Could not format ( { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } Fr No /\ { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } Po No /\ { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } Se No ) : No typesetting found for |- ( { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } Fr No /\ { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } Po No /\ { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } Se No ) with typecode |-
9	4	lrrecpred	Could not format ( x e. No -> Pred ( { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } , No , x ) = ( ( _Left ` x ) u. ( _Right ` x ) ) ) : No typesetting found for |- ( x e. No -> Pred ( { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } , No , x ) = ( ( _Left ` x ) u. ( _Right ` x ) ) ) with typecode |-
10	9	raleqdv	Could not format ( x e. No -> ( A. y e. Pred ( { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } , No , x ) ps <-> A. y e. ( ( _Left ` x ) u. ( _Right ` x ) ) ps ) ) : No typesetting found for |- ( x e. No -> ( A. y e. Pred ( { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } , No , x ) ps <-> A. y e. ( ( _Left ` x ) u. ( _Right ` x ) ) ps ) ) with typecode |-
11	10 3	sylbid	Could not format ( x e. No -> ( A. y e. Pred ( { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } , No , x ) ps -> ph ) ) : No typesetting found for |- ( x e. No -> ( A. y e. Pred ( { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } , No , x ) ps -> ph ) ) with typecode |-
12	11 1 2	frpoins3g	Could not format ( ( ( { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } Fr No /\ { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } Po No /\ { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } Se No ) /\ A e. No ) -> ch ) : No typesetting found for |- ( ( ( { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } Fr No /\ { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } Po No /\ { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } Se No ) /\ A e. No ) -> ch ) with typecode |-
13	8 12	mpan	$$⊢A\in \mathrm{No}\to \chi$$