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	Could not format assertion : No typesetting found for |- ( TC+ A e. V -> ( A =/= (/) <-> (/) e. TC+ A ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ttc00	Could not format ( A = (/) <-> TC+ A = (/) ) : No typesetting found for |- ( A = (/) <-> TC+ A = (/) ) with typecode |-
2	1	necon3bii	Could not format ( A =/= (/) <-> TC+ A =/= (/) ) : No typesetting found for |- ( A =/= (/) <-> TC+ A =/= (/) ) with typecode |-
3		ttctr	Could not format Tr TC+ A : No typesetting found for |- Tr TC+ A with typecode |-
4		tr0elw	Could not format ( ( TC+ A e. V /\ TC+ A =/= (/) /\ Tr TC+ A ) -> (/) e. TC+ A ) : No typesetting found for |- ( ( TC+ A e. V /\ TC+ A =/= (/) /\ Tr TC+ A ) -> (/) e. TC+ A ) with typecode |-
5	3 4	mp3an3	Could not format ( ( TC+ A e. V /\ TC+ A =/= (/) ) -> (/) e. TC+ A ) : No typesetting found for |- ( ( TC+ A e. V /\ TC+ A =/= (/) ) -> (/) e. TC+ A ) with typecode |-
6		ne0i	Could not format ( (/) e. TC+ A -> TC+ A =/= (/) ) : No typesetting found for |- ( (/) e. TC+ A -> TC+ A =/= (/) ) with typecode |-
7	6	adantl	Could not format ( ( TC+ A e. V /\ (/) e. TC+ A ) -> TC+ A =/= (/) ) : No typesetting found for |- ( ( TC+ A e. V /\ (/) e. TC+ A ) -> TC+ A =/= (/) ) with typecode |-
8	5 7	impbida	Could not format ( TC+ A e. V -> ( TC+ A =/= (/) <-> (/) e. TC+ A ) ) : No typesetting found for |- ( TC+ A e. V -> ( TC+ A =/= (/) <-> (/) e. TC+ A ) ) with typecode |-
9	2 8	bitrid	Could not format ( TC+ A e. V -> ( A =/= (/) <-> (/) e. TC+ A ) ) : No typesetting found for |- ( TC+ A e. V -> ( A =/= (/) <-> (/) e. TC+ A ) ) with typecode |-