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

Metamath Proof Explorer

Theorem frins

Description: Well-Founded Induction Schema. If a property passes from all elements less than y of a well-founded class A to y itself (induction hypothesis), then the property holds for all elements of A . (Contributed by Scott Fenton, 6-Feb-2011) (Revised by Mario Carneiro, 26-Jun-2015)

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

Proof

Step	Hyp	Ref	Expression
1		frins.1	$⊢ R Fr A$
2		frins.2	$⊢ R Se A$
3		frins.3	$⊢ y \in A \to (\forall z \in Pred (R, A, y) \underset{˙}{[} z / y \underset{˙}{]} φ \to φ)$
4	3	frinsg	$⊢ (R Fr 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 φ$