Proposition 129, p. 83: If 𝐹 is a function and (for distinct 𝐴 and 𝐵) either 𝐴 follows 𝐵 or 𝐵 follows 𝐴 in the transitive closure of 𝐹, the successor of 𝐴 is either 𝐵 or it follows 𝐵 or it comes before 𝐵 in the #TransitiveClosure of 𝐹.

Hyp. ⊢ (𝜑 → 𝐹 ∈ V)

Hyp. ⊢ (𝜑 → 𝐴 ∈ dom 𝐹)

Hyp. ⊢ (𝜑 → 𝐶 = (𝐹‘𝐴))

Hyp. ⊢ (𝜑 → (𝐴(tc‘𝐹)𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵(tc‘𝐹)𝐴))

Hyp. ⊢ (𝜑 → Fun 𝐹)

Therefore ⊢ (𝜑 → (𝐵(tc‘𝐹)𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶(tc‘𝐹)𝐵))

———

Proposition 131, p. 85: If 𝐹 is a function and 𝐴 contains all elements of 𝑈 and all elements before or after those elements of 𝑈 in the transitive closure of 𝐹, then the image under 𝐹 of 𝐴 is a subclass of 𝐴.

Hyp. ⊢ (𝜑 → 𝐹 ∈ V)

Hyp. ⊢ (𝜑 → 𝐴 = (𝑈 ∪ ((◡(tc‘𝐹) “ 𝑈) ∪ ((tc‘𝐹) “ 𝑈))))

Hyp. ⊢ (𝜑 → Fun 𝐹)

Therefore ⊢ (𝜑 → (𝐹 “ 𝐴) ⊆ 𝐴)

———

Proposition 133, p. 86: If 𝐹 is a function and 𝐴 and 𝐵 both follow 𝑋 in the transitive closure of 𝐹, then (for distinct 𝐴 and 𝐵) either 𝐴 follows 𝐵 or 𝐵 follows 𝐴 in the transitive closure of 𝐹 (or both if it loops).

Hyp. ⊢ (𝜑 → 𝐹 ∈ V)

Hyp. ⊢ (𝜑 → 𝑋(tc‘𝐹)𝐴)

Hyp. ⊢ (𝜑 → 𝑋(tc‘𝐹)𝐵)

Hyp. ⊢ (𝜑 → Fun 𝐹)

Therefore ⊢ (𝜑 → (𝐴(tc‘𝐹)𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵(tc‘𝐹)𝐴))

———

So what's nice about the transitive closure that #Frege felt compelled to invent a new language in which to present mathematical arguments? When 𝑅 is a function, two sets being related by the transitive closure of 𝑅 is much like induction. When 𝑅 is a more general relation, we have a more general form of induction, that is truly #ancestral in the language of #Whitehead and #Russell.

Proposition 111, p. 75: If either 𝐴 and 𝐶 are the same or 𝐶 follows 𝐴 in the transitive closure of 𝑅 and 𝐵 is the successor to 𝐶, then either 𝐴 and 𝐵 are the same or 𝐴 follows 𝐵 or 𝐵 and 𝐴 in the #TransitiveClosure of 𝑅.

Hyp. ⊢ (𝜑 → 𝑅 ∈ V)

Hyp. ⊢ (𝜑 → 𝐴 ∈ V)

Hyp. ⊢ (𝜑 → 𝐵 ∈ V)

Hyp. ⊢ (𝜑 → 𝐶 ∈ V)

Hyp. ⊢ (𝜑 → (𝐴(tc‘𝑅)𝐶 ∨ 𝐴 = 𝐶))

Hyp. ⊢ (𝜑 → 𝐶𝑅𝐵)

Therefore ⊢ (𝜑 → (𝐴(tc‘𝑅)𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵(tc‘𝑅)𝐴))

———

Proposition 122, p. 79: If 𝐹 is a function, 𝐴 is the successor of 𝑋, and 𝐵 is the successor of 𝑋, then 𝐴 and 𝐵 are the same (or 𝐵 follows 𝐴 in the transitive closure of 𝐹).

Hyp. ⊢ (𝜑 → 𝐴 = (𝐹‘𝑋)) ; 𝐴 is the value of 𝐹 (implicitly assumed to be a function) at 𝑋 such that 𝐴 is the unique value that 𝐴 immediately follows 𝑋, 𝑋𝐹𝐴.

Hyp. ⊢ (𝜑 → 𝐵 = (𝐹‘𝑋))

Therefore ⊢ (𝜑 → (𝐴(tc‘𝐹)𝐵 ∨ 𝐴 = 𝐵))

———

Proposition 124, p. 80: If 𝐹 is a function, 𝐴 is the successor of 𝑋, and 𝐵 follows 𝑋 in the transitive closure of 𝐹, then 𝐴 and 𝐵 are the same or 𝐵 follows 𝐴 in the transitive closure of 𝐹.

Hyp. ⊢ (𝜑 → 𝐹 ∈ V)

Hyp. ⊢ (𝜑 → 𝑋 ∈ dom 𝐹) ; 𝑋 is in the domain of relation 𝐹

Hyp. ⊢ (𝜑 → 𝐴 = (𝐹‘𝑋))

Hyp. ⊢ (𝜑 → 𝑋(tc‘𝐹)𝐵)

Hyp. ⊢ (𝜑 → Fun 𝐹) ; relation 𝐹 is a function

Therefore ⊢ (𝜑 → (𝐴(tc‘𝐹)𝐵 ∨ 𝐴 = 𝐵))

———

Proposition 126, p. 81: If 𝐹 is a function, 𝐴 is the successor of 𝑋, and 𝐵 follows 𝑋 in the transitive closure of 𝐹, then (for distinct 𝐴 and 𝐵) either 𝐴 follows 𝐵 or 𝐵 follows 𝐴 in the transitive closure of 𝐹.

Hyp. ⊢ (𝜑 → 𝐹 ∈ V)

Hyp. ⊢ (𝜑 → 𝑋 ∈ dom 𝐹)

Hyp. ⊢ (𝜑 → 𝐴 = (𝐹‘𝑋))

Hyp. ⊢ (𝜑 → 𝑋(tc‘𝐹)𝐵)

Hyp. ⊢ (𝜑 → Fun 𝐹)

Therefore ⊢ (𝜑 → (𝐴(tc‘𝐹)𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵(tc‘𝐹)𝐴))

Proposition 98, p. 71: If 𝐶 follows 𝐴 and 𝐵 follows 𝐶 in the #TransitiveClosure of 𝑅, then 𝐵 follows 𝐴 in the transitive closure of 𝑅.

Hyp. ⊢ (𝜑 → 𝐴 ∈ V)

Hyp. ⊢ (𝜑 → 𝐵 ∈ V)

Hyp. ⊢ (𝜑 → 𝐶 ∈ V)

Hyp. ⊢ (𝜑 → 𝐴(tc‘𝑅)𝐶)

Hyp. ⊢ (𝜑 → 𝐶(tc‘𝑅)𝐵)

Therefore ⊢ (𝜑 → 𝐴(tc‘𝑅)𝐵)

———

Proposition 102, p. 72: If either 𝐴 and 𝐶 are the same or 𝐶 follows 𝐴 in the transitive closure of 𝑅 and 𝐵 is the successor to 𝐶, then 𝐵 follows 𝐴 in the transitive closure of 𝑅.

Hyp. ⊢ (𝜑 → 𝑅 ∈ V)

Hyp. ⊢ (𝜑 → 𝐴 ∈ V)

Hyp. ⊢ (𝜑 → 𝐵 ∈ V)

Hyp. ⊢ (𝜑 → 𝐶 ∈ V)

Hyp. ⊢ (𝜑 → (𝐴(tc‘𝑅)𝐶 ∨ 𝐴 = 𝐶))

Hyp. ⊢ (𝜑 → 𝐶𝑅𝐵)

Therefore ⊢ (𝜑 → 𝐴(tc‘𝑅)𝐵)

———

Proposition 106, p. 73: If 𝐵 follows 𝐴 in 𝑅, then either 𝐴 and 𝐵 are the same or 𝐵 follows 𝐴 in 𝑅.

Hyp. ⊢ (𝜑 → 𝐴𝑅𝐵)

Therefore ⊢ (𝜑 → (𝐴𝑅𝐵 ∨ 𝐴 = 𝐵))

———

Proposition 108, p. 74: If either 𝐴 and 𝐶 are the same or 𝐶 follows 𝐴 in the transitive closure of 𝑅 and 𝐵 is the successor to 𝐶, then either 𝐴 and 𝐵 are the same or 𝐵 follows 𝐴 in the transitive closure of 𝑅.

Hyp. ⊢ (𝜑 → 𝑅 ∈ V)

Hyp. ⊢ (𝜑 → 𝐴 ∈ V)

Hyp. ⊢ (𝜑 → 𝐵 ∈ V)

Hyp. ⊢ (𝜑 → 𝐶 ∈ V)

Hyp. ⊢ (𝜑 → (𝐴(tc‘𝑅)𝐶 ∨ 𝐴 = 𝐶))

Hyp. ⊢ (𝜑 → 𝐶𝑅𝐵)

Therefore ⊢ (𝜑 → (𝐴(tc‘𝑅)𝐵 ∨ 𝐴 = 𝐵))

———

Proposition 109, p. 74: If 𝐴 contains all elements of 𝑈 and all elements after those in 𝑈 in the transitive closure of 𝑅, then the image under 𝑅 of 𝐴 is a subclass of 𝐴.

Hyp. ⊢ (𝜑 → 𝑅 ∈ V)

Hyp. ⊢ (𝜑 → 𝐴 = (𝑈 ∪ ((tc‘𝑅) “ 𝑈)))

Therefore ⊢ (𝜑 → (𝑅 “ 𝐴) ⊆ 𝐴)

———

Proposition 114, p. 76: If either 𝑅 relates 𝐴 and 𝐵 or 𝐴 and 𝐵 are the same, then either 𝐴 and 𝐵 are the same, 𝑅 relates 𝐴 and 𝐵, 𝑅 relates 𝐵 and 𝐴.

Hyp. ⊢ (𝜑 → (𝐴𝑅𝐵 ∨ 𝐴 = 𝐵))

Therefore ⊢ (𝜑 → (𝐴𝑅𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵𝑅𝐴))

Proposition 83, p. 65: If the image of the union of 𝑈 and 𝑊 is a subset of the union of 𝑈 and 𝑊, 𝐴 is an element of 𝑈 and 𝐵 follows 𝐴 in the #TransitiveClosure of 𝑅, then 𝐵 is an element of the union of 𝑈 and 𝑊.

Hyp. ⊢ (𝜑 → 𝑅 ∈ V) ; 𝑅 is a set, i.e. an element of the universal class V (not 𝑉).

Hyp. ⊢ (𝜑 → 𝐴 ∈ 𝑈) ; 𝐴 is an element of class 𝑈.

Hyp. ⊢ (𝜑 → 𝐵 ∈ V) ; 𝐵 is a set.

Hyp. ⊢ (𝜑 → 𝐴(tc‘𝑅)𝐵)

Hyp. ⊢ (𝜑 → (𝑅 “ (𝑈 ∪ 𝑊)) ⊆ (𝑈 ∪ 𝑊)) ; Relation 𝑅 is hereditary in the union of classes 𝑈 and 𝑊.

Therefore ⊢ (𝜑 → 𝐵 ∈ (𝑈 ∪ 𝑊))

———

Proposition 96, p. 71. If 𝐶 follows 𝐴 in the transitive closure of 𝑅 and 𝐵 follows 𝐶 in 𝑅, then 𝐵 follows 𝐴 in the transitive closure of 𝑅.

Hyp. ⊢ (𝜑 → 𝑅 ∈ V)

Hyp. ⊢ (𝜑 → 𝐴 ∈ V)

Hyp. ⊢ (𝜑 → 𝐵 ∈ V)

Hyp. ⊢ (𝜑 → 𝐶 ∈ V)

Hyp. ⊢ (𝜑 → 𝐴(tc‘𝑅)𝐶) ; i.e. 𝐶 eventually follows 𝐴

Hyp. ⊢ (𝜑 → 𝐶𝑅𝐵) ; 𝐵 immediately follows 𝐶

Therefore ⊢ (𝜑 → 𝐴(tc‘𝑅)𝐵)

———

Proposition 87, p. 66: If the images of both {𝐴} and 𝑈 are subsets of 𝑈 and 𝐶 follows 𝐴 in the transitive closure of 𝑅 and 𝐵 follows 𝐶 in 𝑅, then 𝐵 is an element of 𝑈.

Hyp. ⊢ (𝜑 → 𝑅 ∈ V)

Hyp. ⊢ (𝜑 → 𝐴 ∈ V)

Hyp. ⊢ (𝜑 → 𝐵 ∈ V

Hyp. ⊢ (𝜑 → 𝐶 ∈ V)

Hyp. ⊢ (𝜑 → 𝐴(tc‘𝑅)𝐶)

Hyp. ⊢ (𝜑 → 𝐶𝑅𝐵)

Hyp. ⊢ (𝜑 → (𝑅 “ {𝐴}) ⊆ 𝑈)

Hyp. ⊢ (𝜑 → (𝑅 “ 𝑈) ⊆ 𝑈)

Therefore ⊢ (𝜑 → 𝐵 ∈ 𝑈)

———

Proposition 91, p. 68. If 𝐵 follows 𝐴 in 𝑅 then 𝐵 follows 𝐴 in the transitive closure of 𝑅.

Hyp. ⊢ (𝜑 → 𝑅 ∈ V)

Hyp. ⊢ (𝜑 → 𝐴𝑅𝐵)

Therefore ⊢ (𝜑 → 𝐴(tc‘𝑅)𝐵)

———

Proposition 97, p. 71: If 𝐴 contains all elements after those in 𝑈 in the transitive closure of 𝑅, then the image under 𝑅 of 𝐴 is a subclass of 𝐴.

Hyp. ⊢ (𝜑 → 𝑅 ∈ V)

Hyp. ⊢ (𝜑 → 𝐴 = ((tc‘𝑅) “ 𝑈))

Therefore ⊢ (𝜑 → (𝑅 “ 𝐴) ⊆ 𝐴)

Proposition 77, p. 62: If the images of both {𝐴} and 𝑈 are subsets of 𝑈 and 𝐵 follows 𝐴 in the #TransitiveClosure of 𝑅, then 𝐵 is an element of 𝑈.

Hyp. ⊢ (𝜑 → 𝑅 ∈ V) ; 𝑅 is a set, which we newly require so that transitive closure may be a function. Implied, it has relation content. (tc‘𝑅) is its transitive closure, the smallest relation which contains it and has the transitive property.

Hyp. ⊢ (𝜑 → 𝐴 ∈ V) ; 𝐴 is a set.

Hyp. ⊢ (𝜑 → 𝐵 ∈ V) ; 𝐵 is a set.

Hyp. ⊢ (𝜑 → 𝐴(tc‘𝑅)𝐵) ; 𝐴 is related to 𝐵 by the transitive closure of 𝑅

Hyp. ⊢ (𝜑 → (𝑅 “ 𝑈) ⊆ 𝑈) ; The image of class 𝑈 is contained in 𝑈, which means the relation 𝑅 is hereditary in 𝑈

Hyp. ⊢ (𝜑 → (𝑅 “ {𝐴}) ⊆ 𝑈) ; The image of the singleton {𝐴} is contained in 𝑈

Therefore ⊢ (𝜑 → 𝐵 ∈ 𝑈) ; 𝐵 is an element of 𝑈.

———

Proposition 81, p. 63: If the image of 𝑈 is a subset of 𝑈, 𝐴 is an element of 𝑈 and 𝐵 follows 𝐴 in the transitive closure of 𝑅, then 𝐵 is an element of 𝑈.

Hyp. ⊢ (𝜑 → 𝑅 ∈ V)

Hyp. ⊢ (𝜑 → 𝐴 ∈ 𝑈) ; 𝐴 is not just a set, but an element of class 𝑈. This trick allows us to eliminate the last hypothesis of Proposition 77.

Hyp. ⊢ (𝜑 → 𝐵 ∈ V)

Hyp. ⊢ (𝜑 → 𝐴(tc‘𝑅)𝐵)

Hyp. ⊢ (𝜑 → (𝑅 “ 𝑈) ⊆ 𝑈)

Therefore ⊢ (𝜑 → 𝐵 ∈ 𝑈)

Notation guide (adapted from Metamath):

• 𝜑, a metavariable standing for any logical formula, abbreviates the conjunction of all hypotheses listed for a given proposition; writing each line as ⊢ (𝜑 → …) puts the theorem in "deduction form," which can be easier to apply in #Metamath.

• ⊢ 𝜑 asserts that 𝜑 is true; the turnstile is descended from #Frege's own Urteilsstrich (judgment stroke).

• 𝐴𝑅𝐵 means the ordered pair ⟨𝐴, 𝐵⟩ is an element of 𝑅, or we could say 𝐵 immediately follows 𝐴

• 𝐵 = (𝑅‘𝐴) means 𝐵 is the unique set such that 𝐴𝑅𝐵 is true (when such a 𝐵 exists) which means 𝑅 is function-like when restricted to operating on the singleton {𝐴}

• (𝑅”𝐴) is the image of 𝐴

• dom 𝑅 is the domain of 𝑅, the class of all sets 𝑥 such that there is a set 𝑦 that would make 𝑥𝑅𝑦 true.

• Fun 𝑅 is true when 𝑅 is function-like for all sets in its domain.

• ◡𝑅 is the converse of 𝑅 so 𝐴◡𝑅𝐵 iff 𝐵𝑅𝐴

• (tc‘𝑅) is the #TransitiveClosure of 𝑅 (Metamath uses (t+‘𝑅) which can be awkward.) Whitehead and Russell use the term ancestral to describe how 𝐴(tc‘𝑅)𝐵 means 𝐴 is some “ancestor” of 𝐵. Alternately, we can say 𝐵 eventually follows 𝐴.

• V is the universal class, every set is a member, and only sets may be members of any class. After Frege’s later work ran into Russell’s Paradox, it was discovered that not every class {𝑥 | 𝜑} makes sense as a set and so we need the hypothesis ⊢ (𝜑 → 𝐴 ∈ V) before we can talk about the function value of 𝐴 or the ordered pair ⟨𝐴, 𝐵⟩ being an element of 𝑅. V is not italic because it is a constant symbol, like tc, dom, and Fun.