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	|- ( R C_ ( t+ ` R ) \/ ( t+ ` R ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		exmid	|- ( R e. _V \/ -. R e. _V )
2		trclfvlb	|- ( R e. _V -> R C_ ( t+ ` R ) )
3		fvprc	|- ( -. R e. _V -> ( t+ ` R ) = (/) )
4	2 3	orim12i	|- ( ( R e. _V \/ -. R e. _V ) -> ( R C_ ( t+ ` R ) \/ ( t+ ` R ) = (/) ) )
5	1 4	ax-mp	|- ( R C_ ( t+ ` R ) \/ ( t+ ` R ) = (/) )