This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )