Metamath Proof Explorer

Theorem tr0elw

Description: Every nonempty transitive set contains the empty set (/) as an element, a consequence of Regularity. If we assume Transitive Containment, then we can omit the A e. V hypothesis, see tr0el . (Contributed by Matthew House, 6-Apr-2026)

Ref Expression
Assertion tr0elw ⊢ A ∈ V ∧ A ≠ ∅ ∧ Tr ⁡ A → ∅ ∈ A

Proof

Step Hyp Ref Expression
1 zfreg ⊢ A ∈ V ∧ A ≠ ∅ → ∃ x ∈ A x ∩ A = ∅
2 trss ⊢ Tr ⁡ A → x ∈ A → x ⊆ A
3 2 imp ⊢ Tr ⁡ A ∧ x ∈ A → x ⊆ A
4 dfss ⊢ x ⊆ A ↔ x = x ∩ A
5 eqeq2 ⊢ x ∩ A = ∅ → x = x ∩ A ↔ x = ∅
6 4 5 bitrid ⊢ x ∩ A = ∅ → x ⊆ A ↔ x = ∅
7 3 6 syl5ibcom ⊢ Tr ⁡ A ∧ x ∈ A → x ∩ A = ∅ → x = ∅
8 eleq1 ⊢ x = ∅ → x ∈ A ↔ ∅ ∈ A
9 8 biimpcd ⊢ x ∈ A → x = ∅ → ∅ ∈ A
10 9 adantl ⊢ Tr ⁡ A ∧ x ∈ A → x = ∅ → ∅ ∈ A
11 7 10 syld ⊢ Tr ⁡ A ∧ x ∈ A → x ∩ A = ∅ → ∅ ∈ A
12 11 rexlimdva ⊢ Tr ⁡ A → ∃ x ∈ A x ∩ A = ∅ → ∅ ∈ A
13 1 12 syl5com ⊢ A ∈ V ∧ A ≠ ∅ → Tr ⁡ A → ∅ ∈ A
14 13 3impia ⊢ A ∈ V ∧ A ≠ ∅ ∧ Tr ⁡ A → ∅ ∈ A