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

Proof

Step	Hyp	Ref	Expression
1		ttc00	⊢ ( 𝐴 = ∅ ↔ TC+ 𝐴 = ∅ )
2	1	necon3bii	⊢ ( 𝐴 ≠ ∅ ↔ TC+ 𝐴 ≠ ∅ )
3		ttctr	⊢ Tr TC+ 𝐴
4		tr0elw	⊢ ( ( TC+ 𝐴 ∈ 𝑉 ∧ TC+ 𝐴 ≠ ∅ ∧ Tr TC+ 𝐴 ) → ∅ ∈ TC+ 𝐴 )
5	3 4	mp3an3	⊢ ( ( TC+ 𝐴 ∈ 𝑉 ∧ TC+ 𝐴 ≠ ∅ ) → ∅ ∈ TC+ 𝐴 )
6		ne0i	⊢ ( ∅ ∈ TC+ 𝐴 → TC+ 𝐴 ≠ ∅ )
7	6	adantl	⊢ ( ( TC+ 𝐴 ∈ 𝑉 ∧ ∅ ∈ TC+ 𝐴 ) → TC+ 𝐴 ≠ ∅ )
8	5 7	impbida	⊢ ( TC+ 𝐴 ∈ 𝑉 → ( TC+ 𝐴 ≠ ∅ ↔ ∅ ∈ TC+ 𝐴 ) )
9	2 8	bitrid	⊢ ( TC+ 𝐴 ∈ 𝑉 → ( 𝐴 ≠ ∅ ↔ ∅ ∈ TC+ 𝐴 ) )