Theorem ttc0el

Description: A transitive closure contains (/) as an element iff it is nonempty, assuming Regularity and Transitive Containment. (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	ttc0el	Could not format assertion : No typesetting found for |- ( 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		tr0el	Could not format ( ( TC+ A =/= (/) /\ Tr TC+ A ) -> (/) e. TC+ A ) : No typesetting found for |- ( ( TC+ A =/= (/) /\ Tr TC+ A ) -> (/) e. TC+ A ) with typecode |-
5	3 4	mpan2	Could not format ( TC+ A =/= (/) -> (/) e. TC+ A ) : No typesetting found for |- ( 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	5 6	impbii	Could not format ( TC+ A =/= (/) <-> (/) e. TC+ A ) : No typesetting found for |- ( TC+ A =/= (/) <-> (/) e. TC+ A ) with typecode |-
8	2 7	bitri	Could not format ( A =/= (/) <-> (/) e. TC+ A ) : No typesetting found for |- ( A =/= (/) <-> (/) e. TC+ A ) with typecode |-