Metamath Proof Explorer

Theorem axuntco

Description: Derivation of ax-un from ax-tco . Use ax-un instead. (Contributed by Matthew House, 6-Apr-2026) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ax-tco ⊢ ∃ y x ∈ y ∧ ∀ v v ∈ y → ∀ u u ∈ v → u ∈ y
2 elequ1 ⊢ v = x → v ∈ y ↔ x ∈ y
3 elequ2 ⊢ v = x → u ∈ v ↔ u ∈ x
4 3 imbi1d ⊢ v = x → u ∈ v → u ∈ y ↔ u ∈ x → u ∈ y
5 4 albidv ⊢ v = x → ∀ u u ∈ v → u ∈ y ↔ ∀ u u ∈ x → u ∈ y
6 2 5 imbi12d ⊢ v = x → v ∈ y → ∀ u u ∈ v → u ∈ y ↔ x ∈ y → ∀ u u ∈ x → u ∈ y
7 6 spvv ⊢ ∀ v v ∈ y → ∀ u u ∈ v → u ∈ y → x ∈ y → ∀ u u ∈ x → u ∈ y
8 elequ1 ⊢ u = w → u ∈ x ↔ w ∈ x
9 elequ1 ⊢ u = w → u ∈ y ↔ w ∈ y
10 8 9 imbi12d ⊢ u = w → u ∈ x → u ∈ y ↔ w ∈ x → w ∈ y
11 10 spvv ⊢ ∀ u u ∈ x → u ∈ y → w ∈ x → w ∈ y
12 7 11 syl6 ⊢ ∀ v v ∈ y → ∀ u u ∈ v → u ∈ y → x ∈ y → w ∈ x → w ∈ y
13 elequ1 ⊢ v = w → v ∈ y ↔ w ∈ y
14 elequ2 ⊢ v = w → u ∈ v ↔ u ∈ w
15 14 imbi1d ⊢ v = w → u ∈ v → u ∈ y ↔ u ∈ w → u ∈ y
16 15 albidv ⊢ v = w → ∀ u u ∈ v → u ∈ y ↔ ∀ u u ∈ w → u ∈ y
17 13 16 imbi12d ⊢ v = w → v ∈ y → ∀ u u ∈ v → u ∈ y ↔ w ∈ y → ∀ u u ∈ w → u ∈ y
18 17 spvv ⊢ ∀ v v ∈ y → ∀ u u ∈ v → u ∈ y → w ∈ y → ∀ u u ∈ w → u ∈ y
19 elequ1 ⊢ u = z → u ∈ w ↔ z ∈ w
20 elequ1 ⊢ u = z → u ∈ y ↔ z ∈ y
21 19 20 imbi12d ⊢ u = z → u ∈ w → u ∈ y ↔ z ∈ w → z ∈ y
22 21 spvv ⊢ ∀ u u ∈ w → u ∈ y → z ∈ w → z ∈ y
23 18 22 syl6 ⊢ ∀ v v ∈ y → ∀ u u ∈ v → u ∈ y → w ∈ y → z ∈ w → z ∈ y
24 12 23 syl6d ⊢ ∀ v v ∈ y → ∀ u u ∈ v → u ∈ y → x ∈ y → w ∈ x → z ∈ w → z ∈ y
25 24 impcom ⊢ x ∈ y ∧ ∀ v v ∈ y → ∀ u u ∈ v → u ∈ y → w ∈ x → z ∈ w → z ∈ y
26 25 impcomd ⊢ x ∈ y ∧ ∀ v v ∈ y → ∀ u u ∈ v → u ∈ y → z ∈ w ∧ w ∈ x → z ∈ y
27 26 exlimdv ⊢ x ∈ y ∧ ∀ v v ∈ y → ∀ u u ∈ v → u ∈ y → ∃ w z ∈ w ∧ w ∈ x → z ∈ y
28 27 alrimiv ⊢ x ∈ y ∧ ∀ v v ∈ y → ∀ u u ∈ v → u ∈ y → ∀ z ∃ w z ∈ w ∧ w ∈ x → z ∈ y
29 1 28 eximii ⊢ ∃ y ∀ z ∃ w z ∈ w ∧ w ∈ x → z ∈ y