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

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 )