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 \to (φ \leftrightarrow ψ)$
		omsinds.2	$⊢ x = A \to (φ \leftrightarrow χ)$
		omsinds.3	$⊢ x \in ω \to (\forall y \in x ψ \to φ)$
	Assertion	omsinds	$⊢ A \in ω \to χ$

Proof

Step	Hyp	Ref	Expression
1		omsinds.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
2		omsinds.2	$⊢ x = A \to (φ \leftrightarrow χ)$
3		omsinds.3	$⊢ x \in ω \to (\forall y \in x ψ \to φ)$
4		omsson	$⊢ ω \subseteq On$
5		epweon	$⊢ E We On$
6		wess	$⊢ ω \subseteq On \to (E We On \to E We ω)$
7	4 5 6	mp2	$⊢ E We ω$
8		epse	$⊢ E Se ω$
9		trom	$⊢ Tr ω$
10		trpred	$⊢ (Tr ω \land x \in ω) \to Pred (E, ω, x) = x$
11	9 10	mpan	$⊢ x \in ω \to Pred (E, ω, x) = x$
12	11	raleqdv	$⊢ x \in ω \to (\forall y \in Pred (E, ω, x) ψ \leftrightarrow \forall y \in x ψ)$
13	12 3	sylbid	$⊢ x \in ω \to (\forall y \in Pred (E, ω, x) ψ \to φ)$
14	7 8 1 2 13	wfis3	$⊢ A \in ω \to χ$