Theorem frpoins3g

Description: Founded Partial 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 𝐴 ) ∧ 𝐵 ∈ 𝐴 ) → 𝜒 )