Metamath Proof Explorer

Theorem tz9.1ctco

Description: Version of tz9.1c derived from ax-tco . (Contributed by Matthew House, 6-Apr-2026)

Ref Expression
Hypothesis tz9.1ctco.1 ⊢ A ∈ V
Assertion tz9.1ctco ⊢ ⋂ x | A ⊆ x ∧ Tr ⁡ x ∈ V

Proof

Step Hyp Ref Expression
1 tz9.1ctco.1 ⊢ A ∈ V
2 axtco2g ⊢ A ∈ V → ∃ x A ⊆ x ∧ Tr ⁡ x
3 1 2 ax-mp ⊢ ∃ x A ⊆ x ∧ Tr ⁡ x
4 intexab ⊢ ∃ x A ⊆ x ∧ Tr ⁡ x ↔ ⋂ x | A ⊆ x ∧ Tr ⁡ x ∈ V
5 3 4 mpbi ⊢ ⋂ x | A ⊆ x ∧ Tr ⁡ x ∈ V