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	⊢ 𝑅 We 𝐴
	wfis.2	⊢ 𝑅 Se 𝐴
	wfis.3	⊢ ( 𝑦 ∈ 𝐴 → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) [ 𝑧 / 𝑦 ] 𝜑 → 𝜑 ) )
Assertion	wfis	⊢ ( 𝑦 ∈ 𝐴 → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		wfis.1	⊢ 𝑅 We 𝐴
2		wfis.2	⊢ 𝑅 Se 𝐴
3		wfis.3	⊢ ( 𝑦 ∈ 𝐴 → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) [ 𝑧 / 𝑦 ] 𝜑 → 𝜑 ) )
4	3	wfisg	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → ∀ 𝑦 ∈ 𝐴 𝜑 )
5	1 2 4	mp2an	⊢ ∀ 𝑦 ∈ 𝐴 𝜑
6	5	rspec	⊢ ( 𝑦 ∈ 𝐴 → 𝜑 )