Theorem trclfvg

Description: The value of the transitive closure of a relation is a superset or (for proper classes) the empty set. (Contributed by RP, 8-May-2020)

	Ref	Expression
Assertion	trclfvg	⊢ ( 𝑅 ⊆ ( t+ ‘ 𝑅 ) ∨ ( t+ ‘ 𝑅 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		exmid	⊢ ( 𝑅 ∈ V ∨ ¬ 𝑅 ∈ V )
2		trclfvlb	⊢ ( 𝑅 ∈ V → 𝑅 ⊆ ( t+ ‘ 𝑅 ) )
3		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( t+ ‘ 𝑅 ) = ∅ )
4	2 3	orim12i	⊢ ( ( 𝑅 ∈ V ∨ ¬ 𝑅 ∈ V ) → ( 𝑅 ⊆ ( t+ ‘ 𝑅 ) ∨ ( t+ ‘ 𝑅 ) = ∅ ) )
5	1 4	ax-mp	⊢ ( 𝑅 ⊆ ( t+ ‘ 𝑅 ) ∨ ( t+ ‘ 𝑅 ) = ∅ )