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 𝐴 ) ∧ 𝐵 ∈ 𝐴 ) → 𝜒 ) |
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 𝐴 ) ∧ 𝐵 ∈ 𝐴 ) → 𝜒 ) |