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 φ ψ
omsinds.2 x = A φ χ
omsinds.3 x ω y x ψ φ
Assertion omsinds A ω χ

Proof

Step Hyp Ref Expression
1 omsinds.1 x = y φ ψ
2 omsinds.2 x = A φ χ
3 omsinds.3 x ω y x ψ φ
4 omsson ω On
5 epweon E We On
6 wess ω On E We On E We ω
7 4 5 6 mp2 E We ω
8 epse E Se ω
9 trom Tr ω
10 trpred Tr ω x ω Pred E ω x = x
11 9 10 mpan x ω Pred E ω x = x
12 11 raleqdv x ω y Pred E ω x ψ y x ψ
13 12 3 sylbid x ω y Pred E ω x ψ φ
14 7 8 1 2 13 wfis3 A ω χ