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 -> ( ph <-> ps ) )
	noinds.2	|- ( x = A -> ( ph <-> ch ) )
	noinds.3	|- ( x e. No -> ( A. y e. ( ( _Left ` x ) u. ( _Right ` x ) ) ps -> ph ) )
Assertion	noinds	|- ( A e. No -> ch )

Proof

Step	Hyp	Ref	Expression
1		noinds.1	|- ( x = y -> ( ph <-> ps ) )
2		noinds.2	|- ( x = A -> ( ph <-> ch ) )
3		noinds.3	|- ( x e. No -> ( A. y e. ( ( _Left ` x ) u. ( _Right ` x ) ) ps -> ph ) )
4		eqid	|- { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } = { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) }
5	4	lrrecfr	|- { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } Fr No
6	4	lrrecpo	|- { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } Po No
7	4	lrrecse	|- { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } Se No
8	5 6 7	3pm3.2i	|- ( { <. 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 )
9	4	lrrecpred	|- ( x e. No -> Pred ( { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } , No , x ) = ( ( _Left ` x ) u. ( _Right ` x ) ) )
10	9	raleqdv	|- ( 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 ) )
11	10 3	sylbid	|- ( x e. No -> ( A. y e. Pred ( { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } , No , x ) ps -> ph ) )
12	11 1 2	frpoins3g	|- ( ( ( { <. 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 )
13	8 12	mpan	|- ( A e. No -> ch )