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	⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fvex	⊢ ( TC ‘ { 𝑥 } ) ∈ V
2		eleq2	⊢ ( 𝑦 = ( TC ‘ { 𝑥 } ) → ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ ( TC ‘ { 𝑥 } ) ) )
3		treq	⊢ ( 𝑦 = ( TC ‘ { 𝑥 } ) → ( Tr 𝑦 ↔ Tr ( TC ‘ { 𝑥 } ) ) )
4	2 3	anbi12d	⊢ ( 𝑦 = ( TC ‘ { 𝑥 } ) → ( ( 𝑥 ∈ 𝑦 ∧ Tr 𝑦 ) ↔ ( 𝑥 ∈ ( TC ‘ { 𝑥 } ) ∧ Tr ( TC ‘ { 𝑥 } ) ) ) )
5		vsnex	⊢ { 𝑥 } ∈ V
6		tcid	⊢ ( { 𝑥 } ∈ V → { 𝑥 } ⊆ ( TC ‘ { 𝑥 } ) )
7	5 6	ax-mp	⊢ { 𝑥 } ⊆ ( TC ‘ { 𝑥 } )
8		vsnid	⊢ 𝑥 ∈ { 𝑥 }
9	7 8	sselii	⊢ 𝑥 ∈ ( TC ‘ { 𝑥 } )
10		tctr	⊢ Tr ( TC ‘ { 𝑥 } )
11	9 10	pm3.2i	⊢ ( 𝑥 ∈ ( TC ‘ { 𝑥 } ) ∧ Tr ( TC ‘ { 𝑥 } ) )
12	1 4 11	ceqsexv2d	⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ Tr 𝑦 )
13		trss	⊢ ( Tr 𝑦 → ( 𝑧 ∈ 𝑦 → 𝑧 ⊆ 𝑦 ) )
14		df-ss	⊢ ( 𝑧 ⊆ 𝑦 ↔ ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) )
15	13 14	imbitrdi	⊢ ( Tr 𝑦 → ( 𝑧 ∈ 𝑦 → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) ) )
16	15	alrimiv	⊢ ( Tr 𝑦 → ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) ) )
17	16	anim2i	⊢ ( ( 𝑥 ∈ 𝑦 ∧ Tr 𝑦 ) → ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) ) ) )
18	17	eximi	⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ Tr 𝑦 ) → ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) ) ) )
19	12 18	ax-mp	⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) ) )