Theorem exeltr

Description: Every set is a member of a transitive set. This requires ax-inf2 to prove, see tz9.1 . (Contributed by Matthew House, 4-Mar-2026)

	Ref	Expression
Assertion	exeltr	|- E. y ( x e. y /\ A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) )

Proof

Step	Hyp	Ref	Expression
1		fvex	|- ( TC ` { x } ) e. _V
2		eleq2	|- ( y = ( TC ` { x } ) -> ( x e. y <-> x e. ( TC ` { x } ) ) )
3		treq	|- ( y = ( TC ` { x } ) -> ( Tr y <-> Tr ( TC ` { x } ) ) )
4	2 3	anbi12d	|- ( y = ( TC ` { x } ) -> ( ( x e. y /\ Tr y ) <-> ( x e. ( TC ` { x } ) /\ Tr ( TC ` { x } ) ) ) )
5		vsnex	|- { x } e. _V
6		tcid	|- ( { x } e. _V -> { x } C_ ( TC ` { x } ) )
7	5 6	ax-mp	|- { x } C_ ( TC ` { x } )
8		vsnid	|- x e. { x }
9	7 8	sselii	|- x e. ( TC ` { x } )
10		tctr	|- Tr ( TC ` { x } )
11	9 10	pm3.2i	|- ( x e. ( TC ` { x } ) /\ Tr ( TC ` { x } ) )
12	1 4 11	ceqsexv2d	|- E. y ( x e. y /\ Tr y )
13		trss	|- ( Tr y -> ( z e. y -> z C_ y ) )
14		df-ss	|- ( z C_ y <-> A. w ( w e. z -> w e. y ) )
15	13 14	imbitrdi	|- ( Tr y -> ( z e. y -> A. w ( w e. z -> w e. y ) ) )
16	15	alrimiv	|- ( Tr y -> A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) )
17	16	anim2i	|- ( ( x e. y /\ Tr y ) -> ( x e. y /\ A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) ) )
18	17	eximi	|- ( E. y ( x e. y /\ Tr y ) -> E. y ( x e. y /\ A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) ) )
19	12 18	ax-mp	|- E. y ( x e. y /\ A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) )