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	|- A e. _V
Assertion	tz9.1tco	|- E. x ( A C_ x /\ Tr x /\ A. y ( ( A C_ y /\ Tr y ) -> x C_ y ) )

Proof

Step	Hyp	Ref	Expression
1		tz9.1tco.1	|- A e. _V
2	1	tz9.1ctco	|- |^| { y | ( A C_ y /\ Tr y ) } e. _V
3	2	isseti	|- E. x x = |^| { y | ( A C_ y /\ Tr y ) }
4		ssmin	|- A C_ |^| { y | ( A C_ y /\ Tr y ) }
5		sseq2	|- ( x = |^| { y | ( A C_ y /\ Tr y ) } -> ( A C_ x <-> A C_ |^| { y | ( A C_ y /\ Tr y ) } ) )
6	4 5	mpbiri	|- ( x = |^| { y | ( A C_ y /\ Tr y ) } -> A C_ x )
7		treq	|- ( z = y -> ( Tr z <-> Tr y ) )
8	7	ralab2	|- ( A. z e. { y | ( A C_ y /\ Tr y ) } Tr z <-> A. y ( ( A C_ y /\ Tr y ) -> Tr y ) )
9		simpr	|- ( ( A C_ y /\ Tr y ) -> Tr y )
10	8 9	mpgbir	|- A. z e. { y | ( A C_ y /\ Tr y ) } Tr z
11		trint	|- ( A. z e. { y | ( A C_ y /\ Tr y ) } Tr z -> Tr |^| { y | ( A C_ y /\ Tr y ) } )
12	10 11	ax-mp	|- Tr |^| { y | ( A C_ y /\ Tr y ) }
13		treq	|- ( x = |^| { y | ( A C_ y /\ Tr y ) } -> ( Tr x <-> Tr |^| { y | ( A C_ y /\ Tr y ) } ) )
14	12 13	mpbiri	|- ( x = |^| { y | ( A C_ y /\ Tr y ) } -> Tr x )
15		eqimss	|- ( x = |^| { y | ( A C_ y /\ Tr y ) } -> x C_ |^| { y | ( A C_ y /\ Tr y ) } )
16		ssintab	|- ( x C_ |^| { y | ( A C_ y /\ Tr y ) } <-> A. y ( ( A C_ y /\ Tr y ) -> x C_ y ) )
17	15 16	sylib	|- ( x = |^| { y | ( A C_ y /\ Tr y ) } -> A. y ( ( A C_ y /\ Tr y ) -> x C_ y ) )
18	6 14 17	3jca	|- ( x = |^| { y | ( A C_ y /\ Tr y ) } -> ( A C_ x /\ Tr x /\ A. y ( ( A C_ y /\ Tr y ) -> x C_ y ) ) )
19	3 18	eximii	|- E. x ( A C_ x /\ Tr x /\ A. y ( ( A C_ y /\ Tr y ) -> x C_ y ) )