Post #2566011

2026-04-27 06:41 UTC

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 ⊢ (𝜑 → (𝐴𝑅𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵𝑅𝐴))

Replies (1)

@Arpie4Math@mathstodon.xyz 2026-04-27 06:42

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‘𝐹)𝐴))

Open ##2566012