Metamath Proof Explorer


Theorem frpoins3g

Description: Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Hypotheses frpoins3g.1 ( 𝑥𝐴 → ( ∀ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑥 ) 𝜓𝜑 ) )
frpoins3g.2 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
frpoins3g.3 ( 𝑥 = 𝐵 → ( 𝜑𝜒 ) )
Assertion frpoins3g ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ 𝐵𝐴 ) → 𝜒 )

Proof

Step Hyp Ref Expression
1 frpoins3g.1 ( 𝑥𝐴 → ( ∀ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑥 ) 𝜓𝜑 ) )
2 frpoins3g.2 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
3 frpoins3g.3 ( 𝑥 = 𝐵 → ( 𝜑𝜒 ) )
4 1 2 frpoins2g ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) → ∀ 𝑥𝐴 𝜑 )
5 3 rspccva ( ( ∀ 𝑥𝐴 𝜑𝐵𝐴 ) → 𝜒 )
6 4 5 sylan ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ 𝐵𝐴 ) → 𝜒 )