Theorem omsinds

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

	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		predep	|- ( x e. _om -> Pred ( _E , _om , x ) = ( _om i^i x ) )
10		ordom	|- Ord _om
11		ordtr	|- ( Ord _om -> Tr _om )
12		trss	|- ( Tr _om -> ( x e. _om -> x C_ _om ) )
13	10 11 12	mp2b	|- ( x e. _om -> x C_ _om )
14		sseqin2	|- ( x C_ _om <-> ( _om i^i x ) = x )
15	13 14	sylib	|- ( x e. _om -> ( _om i^i x ) = x )
16	9 15	eqtrd	|- ( x e. _om -> Pred ( _E , _om , x ) = x )
17	16	raleqdv	|- ( x e. _om -> ( A. y e. Pred ( _E , _om , x ) ps <-> A. y e. x ps ) )
18	17 3	sylbid	|- ( x e. _om -> ( A. y e. Pred ( _E , _om , x ) ps -> ph ) )
19	7 8 1 2 18	wfis3	|- ( A e. _om -> ch )