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	⊢ ( 𝐴 ∈ ω → 𝜒 )