Metamath Proof Explorer

Theorem axtco1from2

Description: Strong form axtco1 of the Axiom of Transitive Containment, derived from the weak form axtco2 . See ax-tco for more information. As written, the proof uses ax-pr via el , but we could alternatively use ax-pow via elALT2 . Use axtco1 instead. (Contributed by Matthew House, 6-Apr-2026) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion axtco1from2 ⊢ ∃ y x ∈ y ∧ ∀ z z ∈ y → ∀ w w ∈ z → w ∈ y

Proof

Step Hyp Ref Expression
1 elequ1 ⊢ v = x → v ∈ y ↔ x ∈ y
2 1 anbi1d ⊢ v = x → v ∈ y ∧ ∀ z z ∈ y → ∀ w w ∈ z → w ∈ y ↔ x ∈ y ∧ ∀ z z ∈ y → ∀ w w ∈ z → w ∈ y
3 2 exbidv ⊢ v = x → ∃ y v ∈ y ∧ ∀ z z ∈ y → ∀ w w ∈ z → w ∈ y ↔ ∃ y x ∈ y ∧ ∀ z z ∈ y → ∀ w w ∈ z → w ∈ y
4 axtco2 ⊢ ∃ y ∀ z z = u ∨ z ∈ y → ∀ w w ∈ z → w ∈ y
5 orc ⊢ z = u → z = u ∨ z ∈ y
6 elequ2 ⊢ z = u → v ∈ z ↔ v ∈ u
7 6 biimprd ⊢ z = u → v ∈ u → v ∈ z
8 elequ1 ⊢ w = v → w ∈ z ↔ v ∈ z
9 elequ1 ⊢ w = v → w ∈ y ↔ v ∈ y
10 8 9 imbi12d ⊢ w = v → w ∈ z → w ∈ y ↔ v ∈ z → v ∈ y
11 10 spvv ⊢ ∀ w w ∈ z → w ∈ y → v ∈ z → v ∈ y
12 7 11 syl9 ⊢ z = u → ∀ w w ∈ z → w ∈ y → v ∈ u → v ∈ y
13 5 12 embantd ⊢ z = u → z = u ∨ z ∈ y → ∀ w w ∈ z → w ∈ y → v ∈ u → v ∈ y
14 13 spimvw ⊢ ∀ z z = u ∨ z ∈ y → ∀ w w ∈ z → w ∈ y → v ∈ u → v ∈ y
15 14 com12 ⊢ v ∈ u → ∀ z z = u ∨ z ∈ y → ∀ w w ∈ z → w ∈ y → v ∈ y
16 olc ⊢ z ∈ y → z = u ∨ z ∈ y
17 16 imim1i ⊢ z = u ∨ z ∈ y → ∀ w w ∈ z → w ∈ y → z ∈ y → ∀ w w ∈ z → w ∈ y
18 17 alimi ⊢ ∀ z z = u ∨ z ∈ y → ∀ w w ∈ z → w ∈ y → ∀ z z ∈ y → ∀ w w ∈ z → w ∈ y
19 15 18 jca2 ⊢ v ∈ u → ∀ z z = u ∨ z ∈ y → ∀ w w ∈ z → w ∈ y → v ∈ y ∧ ∀ z z ∈ y → ∀ w w ∈ z → w ∈ y
20 19 eximdv ⊢ v ∈ u → ∃ y ∀ z z = u ∨ z ∈ y → ∀ w w ∈ z → w ∈ y → ∃ y v ∈ y ∧ ∀ z z ∈ y → ∀ w w ∈ z → w ∈ y
21 4 20 mpi ⊢ v ∈ u → ∃ y v ∈ y ∧ ∀ z z ∈ y → ∀ w w ∈ z → w ∈ y
22 el ⊢ ∃ u v ∈ u
23 21 22 exlimiiv ⊢ ∃ y v ∈ y ∧ ∀ z z ∈ y → ∀ w w ∈ z → w ∈ y
24 3 23 chvarvv ⊢ ∃ y x ∈ y ∧ ∀ z z ∈ y → ∀ w w ∈ z → w ∈ y