Elektrine lite

← Feed

@Arpie4Math@mathstodon.xyz

Post #2566009

2026-04-27 06:37 UTC

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 ⊒ (πœ‘ β†’ 𝐡 ∈ π‘ˆ)

Replies (1)

  • @Arpie4Math@mathstodon.xyz 2026-04-27 06:39

    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 ⊒ (πœ‘ β†’ (𝑅 β€œ 𝐴) βŠ† 𝐴)

    Open ##2566010