Theorem omsinds

Description: Strong (or "total") induction principle over the finite ordinals. (Contributed by Scott Fenton, 17-Jul-2015) (Proof shortened by BJ, 16-Oct-2024)

	Ref	Expression
Hypotheses	omsinds.1	|- ( x = y -> ( ph <-> ps ) )
	omsinds.2	|- ( x = A -> ( ph <-> ch ) )
	omsinds.3	|- ( x e. _om -> ( A. y e. x ps -> ph ) )
Assertion	omsinds	|- ( A e. _om -> ch )

Proof

Step	Hyp	Ref	Expression
1		omsinds.1	|- ( x = y -> ( ph <-> ps ) )
2		omsinds.2	|- ( x = A -> ( ph <-> ch ) )
3		omsinds.3	|- ( x e. _om -> ( A. y e. x ps -> ph ) )
4		omsson	|- _om C_ On
5		epweon	|- _E We On
6		wess	|- ( _om C_ On -> ( _E We On -> _E We _om ) )
7	4 5 6	mp2	|- _E We _om
8		epse	|- _E Se _om
9		trom	|- Tr _om
10		trpred	|- ( ( Tr _om /\ x e. _om ) -> Pred ( _E , _om , x ) = x )
11	9 10	mpan	|- ( x e. _om -> Pred ( _E , _om , x ) = x )
12	11	raleqdv	|- ( x e. _om -> ( A. y e. Pred ( _E , _om , x ) ps <-> A. y e. x ps ) )
13	12 3	sylbid	|- ( x e. _om -> ( A. y e. Pred ( _E , _om , x ) ps -> ph ) )
14	7 8 1 2 13	wfis3	|- ( A e. _om -> ch )