Description: Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 24-Aug-2022)
Ref | Expression | ||
---|---|---|---|
Hypotheses | frpoins2g.1 | ⊢ ( 𝑦 ∈ 𝐴 → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) 𝜓 → 𝜑 ) ) | |
frpoins2g.3 | ⊢ ( 𝑦 = 𝑧 → ( 𝜑 ↔ 𝜓 ) ) | ||
Assertion | frpoins2g | ⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → ∀ 𝑦 ∈ 𝐴 𝜑 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frpoins2g.1 | ⊢ ( 𝑦 ∈ 𝐴 → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) 𝜓 → 𝜑 ) ) | |
2 | frpoins2g.3 | ⊢ ( 𝑦 = 𝑧 → ( 𝜑 ↔ 𝜓 ) ) | |
3 | nfv | ⊢ Ⅎ 𝑦 𝜓 | |
4 | 1 3 2 | frpoins2fg | ⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → ∀ 𝑦 ∈ 𝐴 𝜑 ) |