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 ∈ ω → χ