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	⊢ ( 𝐴 ≠ ∅ ↔ ∅ ∈ TC+ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ttc00	⊢ ( 𝐴 = ∅ ↔ TC+ 𝐴 = ∅ )
2	1	necon3bii	⊢ ( 𝐴 ≠ ∅ ↔ TC+ 𝐴 ≠ ∅ )
3		ttctr	⊢ Tr TC+ 𝐴
4		tr0el	⊢ ( ( TC+ 𝐴 ≠ ∅ ∧ Tr TC+ 𝐴 ) → ∅ ∈ TC+ 𝐴 )
5	3 4	mpan2	⊢ ( TC+ 𝐴 ≠ ∅ → ∅ ∈ TC+ 𝐴 )
6		ne0i	⊢ ( ∅ ∈ TC+ 𝐴 → TC+ 𝐴 ≠ ∅ )
7	5 6	impbii	⊢ ( TC+ 𝐴 ≠ ∅ ↔ ∅ ∈ TC+ 𝐴 )
8	2 7	bitri	⊢ ( 𝐴 ≠ ∅ ↔ ∅ ∈ TC+ 𝐴 )