Metamath Proof Explorer

Theorem axtco2

Description: Weak form of the Axiom of Transitive Containment. See ax-tco for more information. In particular, this theorem shows the derivation of the weak form from the strong form. (Contributed by Matthew House, 6-Apr-2026)

Ref Expression
Assertion axtco2 ⊢ ∃ y ∀ z z = x ∨ z ∈ y → ∀ w w ∈ z → w ∈ y

Proof

Step Hyp Ref Expression
1 axtco1 ⊢ ∃ y x ∈ y ∧ ∀ z z ∈ y → ∀ w w ∈ z → w ∈ y
2 elequ1 ⊢ z = x → z ∈ y ↔ x ∈ y
3 2 biimprcd ⊢ x ∈ y → z = x → z ∈ y
4 3 imim1d ⊢ x ∈ y → z ∈ y → ∀ w w ∈ z → w ∈ y → z = x → ∀ w w ∈ z → w ∈ y
5 4 alimdv ⊢ x ∈ y → ∀ z z ∈ y → ∀ w w ∈ z → w ∈ y → ∀ z z = x → ∀ w w ∈ z → w ∈ y
6 jao ⊢ z = x → ∀ w w ∈ z → w ∈ y → z ∈ y → ∀ w w ∈ z → w ∈ y → z = x ∨ z ∈ y → ∀ w w ∈ z → w ∈ y
7 6 al2imi ⊢ ∀ z z = x → ∀ w w ∈ z → w ∈ y → ∀ z z ∈ y → ∀ w w ∈ z → w ∈ y → ∀ z z = x ∨ z ∈ y → ∀ w w ∈ z → w ∈ y
8 5 7 syli ⊢ x ∈ y → ∀ z z ∈ y → ∀ w w ∈ z → w ∈ y → ∀ z z = x ∨ z ∈ y → ∀ w w ∈ z → w ∈ y
9 8 imp ⊢ x ∈ y ∧ ∀ z z ∈ y → ∀ w w ∈ z → w ∈ y → ∀ z z = x ∨ z ∈ y → ∀ w w ∈ z → w ∈ y
10 1 9 eximii ⊢ ∃ y ∀ z z = x ∨ z ∈ y → ∀ w w ∈ z → w ∈ y