wfisg

Description: Well-Ordered Induction Schema. If a property passes from all elements less than y of a well-ordered class A to y itself (induction hypothesis), then the property holds for all elements of A . (Contributed by Scott Fenton, 11-Feb-2011) (Proof shortened by Scott Fenton, 17-Nov-2024)

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

Proof

Step	Hyp	Ref	Expression
1		wfisg.1	$⊢ y \in A \to (\forall z \in Pred (R, A, y) \underset{˙}{[} z / y \underset{˙}{]} φ \to φ)$
2		wefr	$⊢ R We A \to R Fr A$
3	2	adantr	$⊢ (R We A \land R Se A) \to R Fr A$
4		weso	$⊢ R We A \to R Or A$
5		sopo	$⊢ R Or A \to R Po A$
6	4 5	syl	$⊢ R We A \to R Po A$
7	6	adantr	$⊢ (R We A \land R Se A) \to R Po A$
8		simpr	$⊢ (R We A \land R Se A) \to R Se A$
9	1	adantl	$⊢ ((R Fr A \land R Po A \land R Se A) \land y \in A) \to (\forall z \in Pred (R, A, y) \underset{˙}{[} z / y \underset{˙}{]} φ \to φ)$
10	9	frpoinsg	$⊢ (R Fr A \land R Po A \land R Se A) \to \forall y \in A φ$
11	3 7 8 10	syl3anc	$⊢ (R We A \land R Se A) \to \forall y \in A φ$

Metamath Proof Explorer

Theorem wfisg

Proof