Metamath Proof Explorer


Theorem wfis3

Description: Well-Ordered Induction schema, using implicit substitution. (Contributed by Scott Fenton, 29-Jan-2011)

Ref Expression
Hypotheses wfis3.1 𝑅 We 𝐴
wfis3.2 𝑅 Se 𝐴
wfis3.3 ( 𝑦 = 𝑧 → ( 𝜑𝜓 ) )
wfis3.4 ( 𝑦 = 𝐵 → ( 𝜑𝜒 ) )
wfis3.5 ( 𝑦𝐴 → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) 𝜓𝜑 ) )
Assertion wfis3 ( 𝐵𝐴𝜒 )

Proof

Step Hyp Ref Expression
1 wfis3.1 𝑅 We 𝐴
2 wfis3.2 𝑅 Se 𝐴
3 wfis3.3 ( 𝑦 = 𝑧 → ( 𝜑𝜓 ) )
4 wfis3.4 ( 𝑦 = 𝐵 → ( 𝜑𝜒 ) )
5 wfis3.5 ( 𝑦𝐴 → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) 𝜓𝜑 ) )
6 1 2 3 5 wfis2 ( 𝑦𝐴𝜑 )
7 4 6 vtoclga ( 𝐵𝐴𝜒 )