Metamath Proof Explorer


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 )