Theorem 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 e. A -> ( A. z e. Pred ( R , A , y ) [. z / y ]. ph -> ph ) )
Assertion	wfisg	|- ( ( R We A /\ R Se A ) -> A. y e. A ph )

Proof

Step	Hyp	Ref	Expression
1		wfisg.1	|- ( y e. A -> ( A. z e. Pred ( R , A , y ) [. z / y ]. ph -> ph ) )
2		wefr	|- ( R We A -> R Fr A )
3	2	adantr	|- ( ( R We A /\ R Se A ) -> R Fr A )
4		weso	|- ( R We A -> R Or A )
5		sopo	|- ( R Or A -> R Po A )
6	4 5	syl	|- ( R We A -> R Po A )
7	6	adantr	|- ( ( R We A /\ R Se A ) -> R Po A )
8		simpr	|- ( ( R We A /\ R Se A ) -> R Se A )
9	1	adantl	|- ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ y e. A ) -> ( A. z e. Pred ( R , A , y ) [. z / y ]. ph -> ph ) )
10	9	frpoinsg	|- ( ( R Fr A /\ R Po A /\ R Se A ) -> A. y e. A ph )
11	3 7 8 10	syl3anc	|- ( ( R We A /\ R Se A ) -> A. y e. A ph )