This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wfis

Description: Well-Ordered Induction Schema. If all elements less than a given set x of the well-ordered class A have a property (induction hypothesis), then all elements of A have that property. (Contributed by Scott Fenton, 29-Jan-2011)

	Ref	Expression
Hypotheses	wfis.1	$⊢ R We A$
	wfis.2	$⊢ R Se A$
	wfis.3	$⊢ y \in A \to (\forall z \in Pred (R, A, y) \underset{˙}{[} z / y \underset{˙}{]} φ \to φ)$
Assertion	wfis	$⊢ y \in A \to φ$

Proof

Step	Hyp	Ref	Expression
1		wfis.1	$⊢ R We A$
2		wfis.2	$⊢ R Se A$
3		wfis.3	$⊢ y \in A \to (\forall z \in Pred (R, A, y) \underset{˙}{[} z / y \underset{˙}{]} φ \to φ)$
4	3	wfisg	$⊢ (R We A \land R Se A) \to \forall y \in A φ$
5	1 2 4	mp2an	$⊢ \forall y \in A φ$
6	5	rspec	$⊢ y \in A \to φ$