Metamath Proof Explorer

Table of Contents - 5.8.6. Principle of transitive induction.

If we have a statement that holds for some element, and a relation between elements that implies if it holds for the first element then it must hold for the second element, the principle of transitive induction shows the statement holds for any element related to the first by the (reflexive-)transitive closure of the relation.

  1. relexpindlem
  2. relexpind
  3. rtrclind