Theorem omsinds

Description: Strong (or "total") induction principle over the finite ordinals. (Contributed by Scott Fenton, 17-Jul-2015)

	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		predep	⊢ ( 𝑥 ∈ ω → Pred ( E , ω , 𝑥 ) = ( ω ∩ 𝑥 ) )
10		ordom	⊢ Ord ω
11		ordtr	⊢ ( Ord ω → Tr ω )
12		trss	⊢ ( Tr ω → ( 𝑥 ∈ ω → 𝑥 ⊆ ω ) )
13	10 11 12	mp2b	⊢ ( 𝑥 ∈ ω → 𝑥 ⊆ ω )
14		sseqin2	⊢ ( 𝑥 ⊆ ω ↔ ( ω ∩ 𝑥 ) = 𝑥 )
15	13 14	sylib	⊢ ( 𝑥 ∈ ω → ( ω ∩ 𝑥 ) = 𝑥 )
16	9 15	eqtrd	⊢ ( 𝑥 ∈ ω → Pred ( E , ω , 𝑥 ) = 𝑥 )
17	16	raleqdv	⊢ ( 𝑥 ∈ ω → ( ∀ 𝑦 ∈ Pred ( E , ω , 𝑥 ) 𝜓 ↔ ∀ 𝑦 ∈ 𝑥 𝜓 ) )
18	17 3	sylbid	⊢ ( 𝑥 ∈ ω → ( ∀ 𝑦 ∈ Pred ( E , ω , 𝑥 ) 𝜓 → 𝜑 ) )
19	7 8 1 2 18	wfis3	⊢ ( 𝐴 ∈ ω → 𝜒 )