Theorem tz9.1tco

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

	Ref	Expression
Hypothesis	tz9.1tco.1	⊢ 𝐴 ∈ V
Assertion	tz9.1tco	⊢ ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀ 𝑦 ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		tz9.1tco.1	⊢ 𝐴 ∈ V
2	1	tz9.1ctco	⊢ ∩ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) } ∈ V
3	2	isseti	⊢ ∃ 𝑥 𝑥 = ∩ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) }
4		ssmin	⊢ 𝐴 ⊆ ∩ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) }
5		sseq2	⊢ ( 𝑥 = ∩ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) } → ( 𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ ∩ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) } ) )
6	4 5	mpbiri	⊢ ( 𝑥 = ∩ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) } → 𝐴 ⊆ 𝑥 )
7		treq	⊢ ( 𝑧 = 𝑦 → ( Tr 𝑧 ↔ Tr 𝑦 ) )
8	7	ralab2	⊢ ( ∀ 𝑧 ∈ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) } Tr 𝑧 ↔ ∀ 𝑦 ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → Tr 𝑦 ) )
9		simpr	⊢ ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → Tr 𝑦 )
10	8 9	mpgbir	⊢ ∀ 𝑧 ∈ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) } Tr 𝑧
11		trint	⊢ ( ∀ 𝑧 ∈ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) } Tr 𝑧 → Tr ∩ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) } )
12	10 11	ax-mp	⊢ Tr ∩ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) }
13		treq	⊢ ( 𝑥 = ∩ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) } → ( Tr 𝑥 ↔ Tr ∩ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) } ) )
14	12 13	mpbiri	⊢ ( 𝑥 = ∩ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) } → Tr 𝑥 )
15		eqimss	⊢ ( 𝑥 = ∩ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) } → 𝑥 ⊆ ∩ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) } )
16		ssintab	⊢ ( 𝑥 ⊆ ∩ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) } ↔ ∀ 𝑦 ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) )
17	15 16	sylib	⊢ ( 𝑥 = ∩ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) } → ∀ 𝑦 ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) )
18	6 14 17	3jca	⊢ ( 𝑥 = ∩ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) } → ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀ 𝑦 ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ) )
19	3 18	eximii	⊢ ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀ 𝑦 ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) )