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 | |- ( A =/= (/) <-> (/) e. TC+ A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ttc00 | |- ( A = (/) <-> TC+ A = (/) ) |
|
| 2 | 1 | necon3bii | |- ( A =/= (/) <-> TC+ A =/= (/) ) |
| 3 | ttctr | |- Tr TC+ A |
|
| 4 | tr0el | |- ( ( TC+ A =/= (/) /\ Tr TC+ A ) -> (/) e. TC+ A ) |
|
| 5 | 3 4 | mpan2 | |- ( TC+ A =/= (/) -> (/) e. TC+ A ) |
| 6 | ne0i | |- ( (/) e. TC+ A -> TC+ A =/= (/) ) |
|
| 7 | 5 6 | impbii | |- ( TC+ A =/= (/) <-> (/) e. TC+ A ) |
| 8 | 2 7 | bitri | |- ( A =/= (/) <-> (/) e. TC+ A ) |