Metamath Proof Explorer

Theorem uniclaxun

Description: A class that is closed under the union operation models the Axiom of Union ax-un . Lemma II.2.4(5) of Kunen2 p. 111. (Contributed by Eric Schmidt, 1-Oct-2025)

Ref Expression
Assertion uniclaxun ⊢ ∀ x ∈ M ⋃ x ∈ M → ∀ x ∈ M ∃ y ∈ M ∀ z ∈ M ∃ w ∈ M z ∈ w ∧ w ∈ x → z ∈ y

Proof

Step Hyp Ref Expression
1 rexex ⊢ ∃ w ∈ M z ∈ w ∧ w ∈ x → ∃ w z ∈ w ∧ w ∈ x
2 eluni ⊢ z ∈ ⋃ x ↔ ∃ w z ∈ w ∧ w ∈ x
3 1 2 sylibr ⊢ ∃ w ∈ M z ∈ w ∧ w ∈ x → z ∈ ⋃ x
4 3 rgenw ⊢ ∀ z ∈ M ∃ w ∈ M z ∈ w ∧ w ∈ x → z ∈ ⋃ x
5 eleq2 ⊢ y = ⋃ x → z ∈ y ↔ z ∈ ⋃ x
6 5 imbi2d ⊢ y = ⋃ x → ∃ w ∈ M z ∈ w ∧ w ∈ x → z ∈ y ↔ ∃ w ∈ M z ∈ w ∧ w ∈ x → z ∈ ⋃ x
7 6 ralbidv ⊢ y = ⋃ x → ∀ z ∈ M ∃ w ∈ M z ∈ w ∧ w ∈ x → z ∈ y ↔ ∀ z ∈ M ∃ w ∈ M z ∈ w ∧ w ∈ x → z ∈ ⋃ x
8 7 rspcev ⊢ ⋃ x ∈ M ∧ ∀ z ∈ M ∃ w ∈ M z ∈ w ∧ w ∈ x → z ∈ ⋃ x → ∃ y ∈ M ∀ z ∈ M ∃ w ∈ M z ∈ w ∧ w ∈ x → z ∈ y
9 4 8 mpan2 ⊢ ⋃ x ∈ M → ∃ y ∈ M ∀ z ∈ M ∃ w ∈ M z ∈ w ∧ w ∈ x → z ∈ y
10 9 ralimi ⊢ ∀ x ∈ M ⋃ x ∈ M → ∀ x ∈ M ∃ y ∈ M ∀ z ∈ M ∃ w ∈ M z ∈ w ∧ w ∈ x → z ∈ y