P. 416 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 41501-41600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ss2iundf 41501*	Subclass theorem for indexed union. (Contributed by RP, 17-Jul-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑦𝑌    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ Ⅎ𝑦𝐶    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ Ⅎ𝑦𝐺    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑌) → 𝐷 = 𝐺)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐺)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷)
Theorem	ss2iundv 41502*	Subclass theorem for indexed union. (Contributed by RP, 17-Jul-2020.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑌) → 𝐷 = 𝐺)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐺)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷)
Theorem	cbviuneq12df 41503*	Rule used to change the bound variables and classes in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by RP, 17-Jul-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝑋    &   ⊢ Ⅎ𝑦𝑌    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ Ⅎ𝑦𝐶    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑦𝐺    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝑋 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝑋) → 𝐵 = 𝐹)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑌) → 𝐷 = 𝐺)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐺)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐷 = 𝐹)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐶 𝐷)
Theorem	cbviuneq12dv 41504*	Rule used to change the bound variables and classes in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by RP, 17-Jul-2020.)
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝑋 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝑋) → 𝐵 = 𝐹)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑌) → 𝐷 = 𝐺)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐺)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐷 = 𝐹)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐶 𝐷)
Theorem	conrel1d 41505	Deduction about composition with a class with no relational content. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 → ◡𝐴 = ∅)    ⇒   ⊢ (𝜑 → (𝐴 ∘ 𝐵) = ∅)
Theorem	conrel2d 41506	Deduction about composition with a class with no relational content. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 → ◡𝐴 = ∅)    ⇒   ⊢ (𝜑 → (𝐵 ∘ 𝐴) = ∅)
21.31.3.1  Transitive relations (not to be confused with transitive classes).
Theorem	trrelind 41507	The intersection of transitive relations is a transitive relation. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 → (𝑅 ∘ 𝑅) ⊆ 𝑅)    &   ⊢ (𝜑 → (𝑆 ∘ 𝑆) ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑇 = (𝑅 ∩ 𝑆))    ⇒   ⊢ (𝜑 → (𝑇 ∘ 𝑇) ⊆ 𝑇)
Theorem	xpintrreld 41508	The intersection of a transitive relation with a Cartesian product is a transitive relation. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 → (𝑅 ∘ 𝑅) ⊆ 𝑅)    &   ⊢ (𝜑 → 𝑆 = (𝑅 ∩ (𝐴 × 𝐵)))    ⇒   ⊢ (𝜑 → (𝑆 ∘ 𝑆) ⊆ 𝑆)
Theorem	restrreld 41509	The restriction of a transitive relation is a transitive relation. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 → (𝑅 ∘ 𝑅) ⊆ 𝑅)    &   ⊢ (𝜑 → 𝑆 = (𝑅 ↾ 𝐴))    ⇒   ⊢ (𝜑 → (𝑆 ∘ 𝑆) ⊆ 𝑆)
Theorem	trrelsuperreldg 41510	Concrete construction of a superclass of relation 𝑅 which is a transitive relation. (Contributed by RP, 25-Dec-2019.)
⊢ (𝜑 → Rel 𝑅)    &   ⊢ (𝜑 → 𝑆 = (dom 𝑅 × ran 𝑅))    ⇒   ⊢ (𝜑 → (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆))
Theorem	trficl 41511*	The class of all transitive relations has the finite intersection property. (Contributed by RP, 1-Jan-2020.) (Proof shortened by RP, 3-Jan-2020.)
⊢ 𝐴 = {𝑧 ∣ (𝑧 ∘ 𝑧) ⊆ 𝑧}    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴
Theorem	cnvtrrel 41512	The converse of a transitive relation is a transitive relation. (Contributed by RP, 25-Dec-2019.)
⊢ ((𝑆 ∘ 𝑆) ⊆ 𝑆 ↔ (◡𝑆 ∘ ◡𝑆) ⊆ ◡𝑆)
Theorem	trrelsuperrel2dg 41513	Concrete construction of a superclass of relation 𝑅 which is a transitive relation. (Contributed by RP, 20-Jul-2020.)
⊢ (𝜑 → 𝑆 = (𝑅 ∪ (dom 𝑅 × ran 𝑅)))    ⇒   ⊢ (𝜑 → (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆))
21.31.3.2  Reflexive closures
Syntax	crcl 41514	Extend class notation with reflexive closure.
class r*
Definition	df-rcl 41515*	Reflexive closure of a relation. This is the smallest superset which has the reflexive property. (Contributed by RP, 5-Jun-2020.)
⊢ r* = (𝑥 ∈ V ↦ ∩ {𝑧 ∣ (𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)})
Theorem	dfrcl2 41516	Reflexive closure of a relation as union with restricted identity relation. (Contributed by RP, 6-Jun-2020.)
⊢ r* = (𝑥 ∈ V ↦ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥))
Theorem	dfrcl3 41517	Reflexive closure of a relation as union of powers of the relation. (Contributed by RP, 6-Jun-2020.)
⊢ r* = (𝑥 ∈ V ↦ ((𝑥↑𝑟0) ∪ (𝑥↑𝑟1)))
Theorem	dfrcl4 41518*	Reflexive closure of a relation as indexed union of powers of the relation. (Contributed by RP, 8-Jun-2020.)
⊢ r* = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ {0, 1} (𝑟↑𝑟𝑛))
21.31.3.3  Finite relationship composition. In order for theorems on the transitive closure of a relation to be grouped together before the concept of continuity, we really need an analogue of ↑𝑟 that works on finite ordinals or finite sets instead of natural numbers.
Theorem	relexp2 41519	A set operated on by the relation exponent to the second power is equal to the composition of the set with itself. (Contributed by RP, 1-Jun-2020.)
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟2) = (𝑅 ∘ 𝑅))
Theorem	relexpnul 41520	If the domain and range of powers of a relation are disjoint then the relation raised to the sum of those exponents is empty. (Contributed by RP, 1-Jun-2020.)
⊢ (((𝑅 ∈ 𝑉 ∧ Rel 𝑅) ∧ (𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)) → ((dom (𝑅↑𝑟𝑁) ∩ ran (𝑅↑𝑟𝑀)) = ∅ ↔ (𝑅↑𝑟(𝑁 + 𝑀)) = ∅))
Theorem	eliunov2 41521*	Membership in the indexed union over operator values where the index varies the second input is equivalent to the existence of at least one index such that the element is a member of that operator value. Generalized from dfrtrclrec2 14848. (Contributed by RP, 1-Jun-2020.)
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟 ↑ 𝑛))    ⇒   ⊢ ((𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉) → (𝑋 ∈ (𝐶‘𝑅) ↔ ∃𝑛 ∈ 𝑁 𝑋 ∈ (𝑅 ↑ 𝑛)))
Theorem	eltrclrec 41522*	Membership in the indexed union of relation exponentiation over the natural numbers is equivalent to the existence of at least one number such that the element is a member of that relationship power. (Contributed by RP, 2-Jun-2020.)
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑟↑𝑟𝑛))    ⇒   ⊢ (𝑅 ∈ 𝑉 → (𝑋 ∈ (𝐶‘𝑅) ↔ ∃𝑛 ∈ ℕ 𝑋 ∈ (𝑅↑𝑟𝑛)))
Theorem	elrtrclrec 41523*	Membership in the indexed union of relation exponentiation over the natural numbers (including zero) is equivalent to the existence of at least one number such that the element is a member of that relationship power. (Contributed by RP, 2-Jun-2020.)
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛))    ⇒   ⊢ (𝑅 ∈ 𝑉 → (𝑋 ∈ (𝐶‘𝑅) ↔ ∃𝑛 ∈ ℕ0 𝑋 ∈ (𝑅↑𝑟𝑛)))
Theorem	briunov2 41524*	Two classes related by the indexed union over operator values where the index varies the second input is equivalent to the existence of at least one index such that the two classes are related by that operator value. (Contributed by RP, 1-Jun-2020.)
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟 ↑ 𝑛))    ⇒   ⊢ ((𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉) → (𝑋(𝐶‘𝑅)𝑌 ↔ ∃𝑛 ∈ 𝑁 𝑋(𝑅 ↑ 𝑛)𝑌))
Theorem	brmptiunrelexpd 41525*	If two elements are connected by an indexed union of relational powers, then they are connected via 𝑛 instances the relation, for some 𝑛. Generalization of dfrtrclrec2 14848. (Contributed by RP, 21-Jul-2020.)
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛))    &   ⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → 𝑁 ⊆ ℕ0)    ⇒   ⊢ (𝜑 → (𝐴(𝐶‘𝑅)𝐵 ↔ ∃𝑛 ∈ 𝑁 𝐴(𝑅↑𝑟𝑛)𝐵))
Theorem	fvmptiunrelexplb0d 41526*	If the indexed union ranges over the zeroth power of the relation, then a restriction of the identity relation is a subset of the appliction of the function to the relation. (Contributed by RP, 22-Jul-2020.)
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛))    &   ⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → 𝑁 ∈ V)    &   ⊢ (𝜑 → 0 ∈ 𝑁)    ⇒   ⊢ (𝜑 → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ (𝐶‘𝑅))
Theorem	fvmptiunrelexplb0da 41527*	If the indexed union ranges over the zeroth power of the relation, then a restriction of the identity relation is a subset of the appliction of the function to the relation. (Contributed by RP, 22-Jul-2020.)
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛))    &   ⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → 𝑁 ∈ V)    &   ⊢ (𝜑 → Rel 𝑅)    &   ⊢ (𝜑 → 0 ∈ 𝑁)    ⇒   ⊢ (𝜑 → ( I ↾ ∪ ∪ 𝑅) ⊆ (𝐶‘𝑅))
Theorem	fvmptiunrelexplb1d 41528*	If the indexed union ranges over the first power of the relation, then the relation is a subset of the appliction of the function to the relation. (Contributed by RP, 22-Jul-2020.)
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛))    &   ⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → 𝑁 ∈ V)    &   ⊢ (𝜑 → 1 ∈ 𝑁)    ⇒   ⊢ (𝜑 → 𝑅 ⊆ (𝐶‘𝑅))
Theorem	brfvid 41529	If two elements are connected by a value of the identity relation, then they are connected via the argument. (Contributed by RP, 21-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → (𝐴( I ‘𝑅)𝐵 ↔ 𝐴𝑅𝐵))
Theorem	brfvidRP 41530	If two elements are connected by a value of the identity relation, then they are connected via the argument. This is an example which uses brmptiunrelexpd 41525. (Contributed by RP, 21-Jul-2020.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → (𝐴( I ‘𝑅)𝐵 ↔ 𝐴𝑅𝐵))
Theorem	fvilbd 41531	A set is a subset of its image under the identity relation. (Contributed by RP, 22-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → 𝑅 ⊆ ( I ‘𝑅))
Theorem	fvilbdRP 41532	A set is a subset of its image under the identity relation. (Contributed by RP, 22-Jul-2020.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → 𝑅 ⊆ ( I ‘𝑅))
Theorem	brfvrcld 41533	If two elements are connected by the reflexive closure of a relation, then they are connected via zero or one instances the relation. (Contributed by RP, 21-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → (𝐴(r*‘𝑅)𝐵 ↔ (𝐴(𝑅↑𝑟0)𝐵 ∨ 𝐴(𝑅↑𝑟1)𝐵)))
Theorem	brfvrcld2 41534	If two elements are connected by the reflexive closure of a relation, then they are equal or related by relation. (Contributed by RP, 21-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → (𝐴(r*‘𝑅)𝐵 ↔ ((𝐴 ∈ (dom 𝑅 ∪ ran 𝑅) ∧ 𝐵 ∈ (dom 𝑅 ∪ ran 𝑅) ∧ 𝐴 = 𝐵) ∨ 𝐴𝑅𝐵)))
Theorem	fvrcllb0d 41535	A restriction of the identity relation is a subset of the reflexive closure of a set. (Contributed by RP, 22-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ (r*‘𝑅))
Theorem	fvrcllb0da 41536	A restriction of the identity relation is a subset of the reflexive closure of a relation. (Contributed by RP, 22-Jul-2020.)
⊢ (𝜑 → Rel 𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → ( I ↾ ∪ ∪ 𝑅) ⊆ (r*‘𝑅))
Theorem	fvrcllb1d 41537	A set is a subset of its image under the reflexive closure. (Contributed by RP, 22-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → 𝑅 ⊆ (r*‘𝑅))
Theorem	brtrclrec 41538*	Two classes related by the indexed union of relation exponentiation over the natural numbers is equivalent to the existence of at least one number such that the two classes are related by that relationship power. (Contributed by RP, 2-Jun-2020.)
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑟↑𝑟𝑛))    ⇒   ⊢ (𝑅 ∈ 𝑉 → (𝑋(𝐶‘𝑅)𝑌 ↔ ∃𝑛 ∈ ℕ 𝑋(𝑅↑𝑟𝑛)𝑌))
Theorem	brrtrclrec 41539*	Two classes related by the indexed union of relation exponentiation over the natural numbers (including zero) is equivalent to the existence of at least one number such that the two classes are related by that relationship power. (Contributed by RP, 2-Jun-2020.)
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛))    ⇒   ⊢ (𝑅 ∈ 𝑉 → (𝑋(𝐶‘𝑅)𝑌 ↔ ∃𝑛 ∈ ℕ0 𝑋(𝑅↑𝑟𝑛)𝑌))
Theorem	briunov2uz 41540*	Two classes related by the indexed union over operator values where the index varies the second input is equivalent to the existence of at least one index such that the two classes are related by that operator value. The index set 𝑁 is restricted to an upper range of integers. (Contributed by RP, 2-Jun-2020.)
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟 ↑ 𝑛))    ⇒   ⊢ ((𝑅 ∈ 𝑈 ∧ 𝑁 = (ℤ≥‘𝑀)) → (𝑋(𝐶‘𝑅)𝑌 ↔ ∃𝑛 ∈ 𝑁 𝑋(𝑅 ↑ 𝑛)𝑌))
Theorem	eliunov2uz 41541*	Membership in the indexed union over operator values where the index varies the second input is equivalent to the existence of at least one index such that the element is a member of that operator value. The index set 𝑁 is restricted to an upper range of integers. (Contributed by RP, 2-Jun-2020.)
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟 ↑ 𝑛))    ⇒   ⊢ ((𝑅 ∈ 𝑈 ∧ 𝑁 = (ℤ≥‘𝑀)) → (𝑋 ∈ (𝐶‘𝑅) ↔ ∃𝑛 ∈ 𝑁 𝑋 ∈ (𝑅 ↑ 𝑛)))
Theorem	ov2ssiunov2 41542*	Any particular operator value is the subset of the index union over a set of operator values. Generalized from rtrclreclem1 14847 and rtrclreclem2 . (Contributed by RP, 4-Jun-2020.)
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟 ↑ 𝑛))    ⇒   ⊢ ((𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉 ∧ 𝑀 ∈ 𝑁) → (𝑅 ↑ 𝑀) ⊆ (𝐶‘𝑅))
Theorem	relexp0eq 41543	The zeroth power of relationships is the same if and only if the union of their domain and ranges is the same. (Contributed by RP, 11-Jun-2020.)
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) → ((dom 𝐴 ∪ ran 𝐴) = (dom 𝐵 ∪ ran 𝐵) ↔ (𝐴↑𝑟0) = (𝐵↑𝑟0)))
Theorem	iunrelexp0 41544*	Simplification of zeroth power of indexed union of powers of relations. (Contributed by RP, 19-Jun-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ⊆ ℕ0 ∧ ({0, 1} ∩ 𝑍) ≠ ∅) → (∪ 𝑥 ∈ 𝑍 (𝑅↑𝑟𝑥)↑𝑟0) = (𝑅↑𝑟0))
Theorem	relexpxpnnidm 41545	Any positive power of a Cartesian product of non-disjoint sets is itself. (Contributed by RP, 13-Jun-2020.)
⊢ (𝑁 ∈ ℕ → ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) ≠ ∅) → ((𝐴 × 𝐵)↑𝑟𝑁) = (𝐴 × 𝐵)))
Theorem	relexpiidm 41546	Any power of any restriction of the identity relation is itself. (Contributed by RP, 12-Jun-2020.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (( I ↾ 𝐴)↑𝑟𝑁) = ( I ↾ 𝐴))
Theorem	relexpss1d 41547	The relational power of a subset is a subset. (Contributed by RP, 17-Jun-2020.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ V)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐴↑𝑟𝑁) ⊆ (𝐵↑𝑟𝑁))
Theorem	comptiunov2i 41548*	The composition two indexed unions is sometimes a similar indexed union. (Contributed by RP, 10-Jun-2020.)
⊢ 𝑋 = (𝑎 ∈ V ↦ ∪ 𝑖 ∈ 𝐼 (𝑎 ↑ 𝑖))    &   ⊢ 𝑌 = (𝑏 ∈ V ↦ ∪ 𝑗 ∈ 𝐽 (𝑏 ↑ 𝑗))    &   ⊢ 𝑍 = (𝑐 ∈ V ↦ ∪ 𝑘 ∈ 𝐾 (𝑐 ↑ 𝑘))    &   ⊢ 𝐼 ∈ V    &   ⊢ 𝐽 ∈ V    &   ⊢ 𝐾 = (𝐼 ∪ 𝐽)    &   ⊢ ∪ 𝑘 ∈ 𝐼 (𝑑 ↑ 𝑘) ⊆ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)    &   ⊢ ∪ 𝑘 ∈ 𝐽 (𝑑 ↑ 𝑘) ⊆ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)    &   ⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) ⊆ ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘)    ⇒   ⊢ (𝑋 ∘ 𝑌) = 𝑍
Theorem	corclrcl 41549	The reflexive closure is idempotent. (Contributed by RP, 13-Jun-2020.)
⊢ (r* ∘ r*) = r*
Theorem	iunrelexpmin1 41550*	The indexed union of relation exponentiation over the natural numbers is the minimum transitive relation that includes the relation. (Contributed by RP, 4-Jun-2020.)
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛))    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ) → ∀𝑠((𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → (𝐶‘𝑅) ⊆ 𝑠))
Theorem	relexpmulnn 41551	With exponents limited to the counting numbers, the composition of powers of a relation is the relation raised to the product of exponents. (Contributed by RP, 13-Jun-2020.)
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾)) ∧ (𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼))
Theorem	relexpmulg 41552	With ordered exponents, the composition of powers of a relation is the relation raised to the product of exponents. (Contributed by RP, 13-Jun-2020.)
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) ∧ (𝐽 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼))
Theorem	trclrelexplem 41553*	The union of relational powers to positive multiples of 𝑁 is a subset to the transitive closure raised to the power of 𝑁. (Contributed by RP, 15-Jun-2020.)
⊢ (𝑁 ∈ ℕ → ∪ 𝑘 ∈ ℕ ((𝐷↑𝑟𝑘)↑𝑟𝑁) ⊆ (∪ 𝑗 ∈ ℕ (𝐷↑𝑟𝑗)↑𝑟𝑁))
Theorem	iunrelexpmin2 41554*	The indexed union of relation exponentiation over the natural numbers (including zero) is the minimum reflexive-transitive relation that includes the relation. (Contributed by RP, 4-Jun-2020.)
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛))    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ0) → ∀𝑠((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → (𝐶‘𝑅) ⊆ 𝑠))
Theorem	relexp01min 41555	With exponents limited to 0 and 1, the composition of powers of a relation is the relation raised to the minimum of exponents. (Contributed by RP, 12-Jun-2020.)
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) ∧ (𝐽 ∈ {0, 1} ∧ 𝐾 ∈ {0, 1})) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼))
Theorem	relexp1idm 41556	Repeated raising a relation to the first power is idempotent. (Contributed by RP, 12-Jun-2020.)
⊢ (𝑅 ∈ 𝑉 → ((𝑅↑𝑟1)↑𝑟1) = (𝑅↑𝑟1))
Theorem	relexp0idm 41557	Repeated raising a relation to the zeroth power is idempotent. (Contributed by RP, 12-Jun-2020.)
⊢ (𝑅 ∈ 𝑉 → ((𝑅↑𝑟0)↑𝑟0) = (𝑅↑𝑟0))
Theorem	relexp0a 41558	Absorbtion law for zeroth power of a relation. (Contributed by RP, 17-Jun-2020.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝐴↑𝑟𝑁)↑𝑟0) ⊆ (𝐴↑𝑟0))
Theorem	relexpxpmin 41559	The composition of powers of a Cartesian product of non-disjoint sets is the Cartesian product raised to the minimum exponent. (Contributed by RP, 13-Jun-2020.)
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) ≠ ∅) ∧ (𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾) ∧ 𝐽 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0)) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼))
Theorem	relexpaddss 41560	The composition of two powers of a relation is a subset of the relation raised to the sum of those exponents. This is equality where 𝑅 is a relation as shown by relexpaddd 14844 or when the sum of the powers isn't 1 as shown by relexpaddg 14843. (Contributed by RP, 3-Jun-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) ⊆ (𝑅↑𝑟(𝑁 + 𝑀)))
Theorem	iunrelexpuztr 41561*	The indexed union of relation exponentiation over upper integers is a transive relation. Generalized from rtrclreclem3 14850. (Contributed by RP, 4-Jun-2020.)
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛))    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 = (ℤ≥‘𝑀) ∧ 𝑀 ∈ ℕ0) → ((𝐶‘𝑅) ∘ (𝐶‘𝑅)) ⊆ (𝐶‘𝑅))
21.31.3.4  Transitive closure of a relation
Theorem	dftrcl3 41562*	Transitive closure of a relation, expressed as indexed union of powers of relations. (Contributed by RP, 5-Jun-2020.)
⊢ t+ = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑟↑𝑟𝑛))
Theorem	brfvtrcld 41563*	If two elements are connected by the transitive closure of a relation, then they are connected via 𝑛 instances the relation, for some counting number 𝑛. (Contributed by RP, 22-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → (𝐴(t+‘𝑅)𝐵 ↔ ∃𝑛 ∈ ℕ 𝐴(𝑅↑𝑟𝑛)𝐵))
Theorem	fvtrcllb1d 41564	A set is a subset of its image under the transitive closure. (Contributed by RP, 22-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → 𝑅 ⊆ (t+‘𝑅))
Theorem	trclfvcom 41565	The transitive closure of a relation commutes with the relation. (Contributed by RP, 18-Jul-2020.)
⊢ (𝑅 ∈ 𝑉 → ((t+‘𝑅) ∘ 𝑅) = (𝑅 ∘ (t+‘𝑅)))
Theorem	cnvtrclfv 41566	The converse of the transitive closure is equal to the transitive closure of the converse relation. (Contributed by RP, 19-Jul-2020.)
⊢ (𝑅 ∈ 𝑉 → ◡(t+‘𝑅) = (t+‘◡𝑅))
Theorem	cotrcltrcl 41567	The transitive closure is idempotent. (Contributed by RP, 16-Jun-2020.)
⊢ (t+ ∘ t+) = t+
Theorem	trclimalb2 41568	Lower bound for image under a transitive closure. (Contributed by RP, 1-Jul-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ (𝑅 “ (𝐴 ∪ 𝐵)) ⊆ 𝐵) → ((t+‘𝑅) “ 𝐴) ⊆ 𝐵)
Theorem	brtrclfv2 41569*	Two ways to indicate two elements are related by the transitive closure of a relation. (Contributed by RP, 1-Jul-2020.)
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑋(t+‘𝑅)𝑌 ↔ 𝑌 ∈ ∩ {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓}))
Theorem	trclfvdecomr 41570	The transitive closure of a relation may be decomposed into a union of the relation and the composition of the relation with its transitive closure. (Contributed by RP, 18-Jul-2020.)
⊢ (𝑅 ∈ 𝑉 → (t+‘𝑅) = (𝑅 ∪ ((t+‘𝑅) ∘ 𝑅)))
Theorem	trclfvdecoml 41571	The transitive closure of a relation may be decomposed into a union of the relation and the composition of the relation with its transitive closure. (Contributed by RP, 18-Jul-2020.)
⊢ (𝑅 ∈ 𝑉 → (t+‘𝑅) = (𝑅 ∪ (𝑅 ∘ (t+‘𝑅))))
Theorem	dmtrclfvRP 41572	The domain of the transitive closure is equal to the domain of the relation. (Contributed by RP, 18-Jul-2020.) (Proof modification is discouraged.)
⊢ (𝑅 ∈ 𝑉 → dom (t+‘𝑅) = dom 𝑅)
Theorem	rntrclfvRP 41573	The range of the transitive closure is equal to the range of the relation. (Contributed by RP, 19-Jul-2020.) (Proof modification is discouraged.)
⊢ (𝑅 ∈ 𝑉 → ran (t+‘𝑅) = ran 𝑅)
Theorem	rntrclfv 41574	The range of the transitive closure is equal to the range of the relation. (Contributed by RP, 18-Jul-2020.) (Proof modification is discouraged.)
⊢ (𝑅 ∈ 𝑉 → ran (t+‘𝑅) = ran 𝑅)
Theorem	dfrtrcl3 41575*	Reflexive-transitive closure of a relation, expressed as indexed union of powers of relations. Generalized from dfrtrcl2 14852. (Contributed by RP, 5-Jun-2020.)
⊢ t* = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛))
Theorem	brfvrtrcld 41576*	If two elements are connected by the reflexive-transitive closure of a relation, then they are connected via 𝑛 instances the relation, for some natural number 𝑛. Similar of dfrtrclrec2 14848. (Contributed by RP, 22-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → (𝐴(t*‘𝑅)𝐵 ↔ ∃𝑛 ∈ ℕ0 𝐴(𝑅↑𝑟𝑛)𝐵))
Theorem	fvrtrcllb0d 41577	A restriction of the identity relation is a subset of the reflexive-transitive closure of a set. (Contributed by RP, 22-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ (t*‘𝑅))
Theorem	fvrtrcllb0da 41578	A restriction of the identity relation is a subset of the reflexive-transitive closure of a relation. (Contributed by RP, 22-Jul-2020.)
⊢ (𝜑 → Rel 𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → ( I ↾ ∪ ∪ 𝑅) ⊆ (t*‘𝑅))
Theorem	fvrtrcllb1d 41579	A set is a subset of its image under the reflexive-transitive closure. (Contributed by RP, 22-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → 𝑅 ⊆ (t*‘𝑅))
Theorem	dfrtrcl4 41580	Reflexive-transitive closure of a relation, expressed as the union of the zeroth power and the transitive closure. (Contributed by RP, 5-Jun-2020.)
⊢ t* = (𝑟 ∈ V ↦ ((𝑟↑𝑟0) ∪ (t+‘𝑟)))
Theorem	corcltrcl 41581	The composition of the reflexive and transitive closures is the reflexive-transitive closure. (Contributed by RP, 17-Jun-2020.)
⊢ (r* ∘ t+) = t*
Theorem	cortrcltrcl 41582	Composition with the reflexive-transitive closure absorbs the transitive closure. (Contributed by RP, 13-Jun-2020.)
⊢ (t* ∘ t+) = t*
Theorem	corclrtrcl 41583	Composition with the reflexive-transitive closure absorbs the reflexive closure. (Contributed by RP, 13-Jun-2020.)
⊢ (r* ∘ t*) = t*
Theorem	cotrclrcl 41584	The composition of the reflexive and transitive closures is the reflexive-transitive closure. (Contributed by RP, 21-Jun-2020.)
⊢ (t+ ∘ r*) = t*
Theorem	cortrclrcl 41585	Composition with the reflexive-transitive closure absorbs the reflexive closure. (Contributed by RP, 13-Jun-2020.)
⊢ (t* ∘ r*) = t*
Theorem	cotrclrtrcl 41586	Composition with the reflexive-transitive closure absorbs the transitive closure. (Contributed by RP, 13-Jun-2020.)
⊢ (t+ ∘ t*) = t*
Theorem	cortrclrtrcl 41587	The reflexive-transitive closure is idempotent. (Contributed by RP, 13-Jun-2020.)
⊢ (t* ∘ t*) = t*
21.31.3.5  Adapted from Frege Theorems inspired by Begriffsschrift without restricting form and content to closely parallel those in [Frege1879].
Theorem	frege77d 41588	If the images of both {𝐴} and 𝑈 are subsets of 𝑈 and 𝐵 follows 𝐴 in the transitive closure of 𝑅, then 𝐵 is an element of 𝑈. Similar to Proposition 77 of [Frege1879] p. 62. Compare with frege77 41782. (Contributed by RP, 15-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → 𝐵 ∈ V)    &   ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐵)    &   ⊢ (𝜑 → (𝑅 “ 𝑈) ⊆ 𝑈)    &   ⊢ (𝜑 → (𝑅 “ {𝐴}) ⊆ 𝑈)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝑈)
Theorem	frege81d 41589	If the image of 𝑈 is a subset 𝑈, 𝐴 is an element of 𝑈 and 𝐵 follows 𝐴 in the transitive closure of 𝑅, then 𝐵 is an element of 𝑈. Similar to Proposition 81 of [Frege1879] p. 63. Compare with frege81 41786. (Contributed by RP, 15-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ V)    &   ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐵)    &   ⊢ (𝜑 → (𝑅 “ 𝑈) ⊆ 𝑈)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝑈)
Theorem	frege83d 41590	If the image of the union of 𝑈 and 𝑉 is a subset of the union of 𝑈 and 𝑉, 𝐴 is an element of 𝑈 and 𝐵 follows 𝐴 in the transitive closure of 𝑅, then 𝐵 is an element of the union of 𝑈 and 𝑉. Similar to Proposition 83 of [Frege1879] p. 65. Compare with frege83 41788. (Contributed by RP, 15-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ V)    &   ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐵)    &   ⊢ (𝜑 → (𝑅 “ (𝑈 ∪ 𝑉)) ⊆ (𝑈 ∪ 𝑉))    ⇒   ⊢ (𝜑 → 𝐵 ∈ (𝑈 ∪ 𝑉))
Theorem	frege96d 41591	If 𝐶 follows 𝐴 in the transitive closure of 𝑅 and 𝐵 follows 𝐶 in 𝑅, then 𝐵 follows 𝐴 in the transitive closure of 𝑅. Similar to Proposition 96 of [Frege1879] p. 71. Compare with frege96 41801. (Contributed by RP, 15-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → 𝐵 ∈ V)    &   ⊢ (𝜑 → 𝐶 ∈ V)    &   ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐶)    &   ⊢ (𝜑 → 𝐶𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐵)
Theorem	frege87d 41592	If the images of both {𝐴} and 𝑈 are subsets of 𝑈 and 𝐶 follows 𝐴 in the transitive closure of 𝑅 and 𝐵 follows 𝐶 in 𝑅, then 𝐵 is an element of 𝑈. Similar to Proposition 87 of [Frege1879] p. 66. Compare with frege87 41792. (Contributed by RP, 15-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → 𝐵 ∈ V)    &   ⊢ (𝜑 → 𝐶 ∈ V)    &   ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐶)    &   ⊢ (𝜑 → 𝐶𝑅𝐵)    &   ⊢ (𝜑 → (𝑅 “ {𝐴}) ⊆ 𝑈)    &   ⊢ (𝜑 → (𝑅 “ 𝑈) ⊆ 𝑈)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝑈)
Theorem	frege91d 41593	If 𝐵 follows 𝐴 in 𝑅 then 𝐵 follows 𝐴 in the transitive closure of 𝑅. Similar to Proposition 91 of [Frege1879] p. 68. Comparw with frege91 41796. (Contributed by RP, 15-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐵)
Theorem	frege97d 41594	If 𝐴 contains all elements after those in 𝑈 in the transitive closure of 𝑅, then the image under 𝑅 of 𝐴 is a subclass of 𝐴. Similar to Proposition 97 of [Frege1879] p. 71. Compare with frege97 41802. (Contributed by RP, 15-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → 𝐴 = ((t+‘𝑅) “ 𝑈))    ⇒   ⊢ (𝜑 → (𝑅 “ 𝐴) ⊆ 𝐴)
Theorem	frege98d 41595	If 𝐶 follows 𝐴 and 𝐵 follows 𝐶 in the transitive closure of 𝑅, then 𝐵 follows 𝐴 in the transitive closure of 𝑅. Similar to Proposition 98 of [Frege1879] p. 71. Compare with frege98 41803. (Contributed by RP, 15-Jul-2020.)
⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → 𝐵 ∈ V)    &   ⊢ (𝜑 → 𝐶 ∈ V)    &   ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐶)    &   ⊢ (𝜑 → 𝐶(t+‘𝑅)𝐵)    ⇒   ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐵)
Theorem	frege102d 41596	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 𝑅. Similar to Proposition 102 of [Frege1879] p. 72. Compare with frege102 41807. (Contributed by RP, 15-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → 𝐵 ∈ V)    &   ⊢ (𝜑 → 𝐶 ∈ V)    &   ⊢ (𝜑 → (𝐴(t+‘𝑅)𝐶 ∨ 𝐴 = 𝐶))    &   ⊢ (𝜑 → 𝐶𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐵)
Theorem	frege106d 41597	If 𝐵 follows 𝐴 in 𝑅, then either 𝐴 and 𝐵 are the same or 𝐵 follows 𝐴 in 𝑅. Similar to Proposition 106 of [Frege1879] p. 73. Compare with frege106 41811. (Contributed by RP, 15-Jul-2020.)
⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ∨ 𝐴 = 𝐵))
Theorem	frege108d 41598	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 𝑅. Similar to Proposition 108 of [Frege1879] p. 74. Compare with frege108 41813. (Contributed by RP, 15-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → 𝐵 ∈ V)    &   ⊢ (𝜑 → 𝐶 ∈ V)    &   ⊢ (𝜑 → (𝐴(t+‘𝑅)𝐶 ∨ 𝐴 = 𝐶))    &   ⊢ (𝜑 → 𝐶𝑅𝐵)    ⇒   ⊢ (𝜑 → (𝐴(t+‘𝑅)𝐵 ∨ 𝐴 = 𝐵))
Theorem	frege109d 41599	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 𝐴. Similar to Proposition 109 of [Frege1879] p. 74. Compare with frege109 41814. (Contributed by RP, 15-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → 𝐴 = (𝑈 ∪ ((t+‘𝑅) “ 𝑈)))    ⇒   ⊢ (𝜑 → (𝑅 “ 𝐴) ⊆ 𝐴)
Theorem	frege114d 41600	If either 𝑅 relates 𝐴 and 𝐵 or 𝐴 and 𝐵 are the same, then either 𝐴 and 𝐵 are the same, 𝑅 relates 𝐴 and 𝐵, 𝑅 relates 𝐵 and 𝐴. Similar to Proposition 114 of [Frege1879] p. 76. Compare with frege114 41819. (Contributed by RP, 15-Jul-2020.)
⊢ (𝜑 → (𝐴𝑅𝐵 ∨ 𝐴 = 𝐵))    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵𝑅𝐴))