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	$$⊢\left(R\subseteq \mathrm{t+}\left(R\right)\vee \mathrm{t+}\left(R\right)=\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		exmid	$$⊢\left(R\in \mathrm{V}\vee \neg R\in \mathrm{V}\right)$$
2		trclfvlb	$$⊢R\in \mathrm{V}\to R\subseteq \mathrm{t+}\left(R\right)$$
3		fvprc	$$⊢\neg R\in \mathrm{V}\to \mathrm{t+}\left(R\right)=\varnothing$$
4	2 3	orim12i	$$⊢\left(R\in \mathrm{V}\vee \neg R\in \mathrm{V}\right)\to \left(R\subseteq \mathrm{t+}\left(R\right)\vee \mathrm{t+}\left(R\right)=\varnothing \right)$$
5	1 4	ax-mp	$$⊢\left(R\subseteq \mathrm{t+}\left(R\right)\vee \mathrm{t+}\left(R\right)=\varnothing \right)$$