Theorem ttc0elw

Description: If a transitive closure is a set, then it contains (/) as an element iff it is nonempty, assuming Regularity. If we also assume Transitive Containment, then we can remove the TC+ A e. V hypothesis, see ttc0el . (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	ttc0elw	|- ( TC+ A e. V -> ( A =/= (/) <-> (/) e. TC+ A ) )

Proof

Step	Hyp	Ref	Expression
1		ttc00	|- ( A = (/) <-> TC+ A = (/) )
2	1	necon3bii	|- ( A =/= (/) <-> TC+ A =/= (/) )
3		ttctr	|- Tr TC+ A
4		tr0elw	|- ( ( TC+ A e. V /\ TC+ A =/= (/) /\ Tr TC+ A ) -> (/) e. TC+ A )
5	3 4	mp3an3	|- ( ( TC+ A e. V /\ TC+ A =/= (/) ) -> (/) e. TC+ A )
6		ne0i	|- ( (/) e. TC+ A -> TC+ A =/= (/) )
7	6	adantl	|- ( ( TC+ A e. V /\ (/) e. TC+ A ) -> TC+ A =/= (/) )
8	5 7	impbida	|- ( TC+ A e. V -> ( TC+ A =/= (/) <-> (/) e. TC+ A ) )
9	2 8	bitrid	|- ( TC+ A e. V -> ( A =/= (/) <-> (/) e. TC+ A ) )