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 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
omsinds.2 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜒 ) )
omsinds.3 ⊢ ( 𝑥 ∈ ω → ( ∀ 𝑦 ∈ 𝑥 𝜓 → 𝜑 ) )
Assertion omsinds ( 𝐴 ∈ ω → 𝜒 )

Proof

Step Hyp Ref Expression
1 omsinds.1 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2 omsinds.2 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜒 ) )
3 omsinds.3 ⊢ ( 𝑥 ∈ ω → ( ∀ 𝑦 ∈ 𝑥 𝜓 → 𝜑 ) )
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 ω ∧ 𝑥 ∈ ω ) → Pred ( E , ω , 𝑥 ) = 𝑥 )
11 9 10 mpan ⊢ ( 𝑥 ∈ ω → Pred ( E , ω , 𝑥 ) = 𝑥 )
12 11 raleqdv ⊢ ( 𝑥 ∈ ω → ( ∀ 𝑦 ∈ Pred ( E , ω , 𝑥 ) 𝜓 ↔ ∀ 𝑦 ∈ 𝑥 𝜓 ) )
13 12 3 sylbid ⊢ ( 𝑥 ∈ ω → ( ∀ 𝑦 ∈ Pred ( E , ω , 𝑥 ) 𝜓 → 𝜑 ) )
14 7 8 1 2 13 wfis3 ⊢ ( 𝐴 ∈ ω → 𝜒 )