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

Proof

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