Metamath Proof Explorer

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 ⊢ ∃ y x ∈ y ∧ ∀ z z ∈ y → ∀ w w ∈ z → w ∈ y

Proof

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