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

Proof

Step Hyp Ref Expression
1 wfisg.1 ⊢ ( 𝑦 ∈ 𝐴 → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) [ 𝑧 / 𝑦 ] 𝜑 → 𝜑 ) )
2 wefr ⊢ ( 𝑅 We 𝐴 → 𝑅 Fr 𝐴 )
3 2 adantr ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝑅 Fr 𝐴 )
4 weso ⊢ ( 𝑅 We 𝐴 → 𝑅 Or 𝐴 )
5 sopo ⊢ ( 𝑅 Or 𝐴 → 𝑅 Po 𝐴 )
6 4 5 syl ⊢ ( 𝑅 We 𝐴 → 𝑅 Po 𝐴 )
7 6 adantr ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝑅 Po 𝐴 )
8 simpr ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝑅 Se 𝐴 )
9 1 adantl ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) [ 𝑧 / 𝑦 ] 𝜑 → 𝜑 ) )
10 9 frpoinsg ⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → ∀ 𝑦 ∈ 𝐴 𝜑 )
11 3 7 8 10 syl3anc ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → ∀ 𝑦 ∈ 𝐴 𝜑 )