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	⊢ 𝐴 ∈ V
Assertion	tz9.1ctco	⊢ ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } ∈ V

Proof

Step	Hyp	Ref	Expression
1		tz9.1ctco.1	⊢ 𝐴 ∈ V
2		axtco2g	⊢ ( 𝐴 ∈ V → ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) )
3	1 2	ax-mp	⊢ ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 )
4		intexab	⊢ ( ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) ↔ ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } ∈ V )
5	3 4	mpbi	⊢ ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } ∈ V