Theorem uniclaxun 45715

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

Assertion

Ref	Expression
uniclaxun	⊢ (∀𝑥 ∈ 𝑀 ∪ 𝑥 ∈ 𝑀 → ∀𝑥 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))

Distinct variable groups:   𝑥,𝑤,𝑦,𝑧   𝑦,𝑀

Allowed substitution hints:   𝑀(𝑥,𝑧,𝑤)

Proof of Theorem uniclaxun

Step	Hyp	Ref	Expression
1		rexex 3095	. . . . 5 ⊢ (∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))
2		eluni 4875	. . . . 5 ⊢ (𝑧 ∈ ∪ 𝑥 ↔ ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))
3	1, 2	sylibr 237	. . . 4 ⊢ (∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ ∪ 𝑥)
4	3	rgenw 3083	. . 3 ⊢ ∀𝑧 ∈ 𝑀 (∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ ∪ 𝑥)
5		eleq2 2852	. . . . . 6 ⊢ (𝑦 = ∪ 𝑥 → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ ∪ 𝑥))
6	5	imbi2d 343	. . . . 5 ⊢ (𝑦 = ∪ 𝑥 → ((∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ (∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ ∪ 𝑥)))
7	6	ralbidv 3188	. . . 4 ⊢ (𝑦 = ∪ 𝑥 → (∀𝑧 ∈ 𝑀 (∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ∀𝑧 ∈ 𝑀 (∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ ∪ 𝑥)))
8	7	rspcev 3581	. . 3 ⊢ ((∪ 𝑥 ∈ 𝑀 ∧ ∀𝑧 ∈ 𝑀 (∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ ∪ 𝑥)) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))
9	4, 8	mpan2 703	. 2 ⊢ (∪ 𝑥 ∈ 𝑀 → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))
10	9	ralimi 3102	1 ⊢ (∀𝑥 ∈ 𝑀 ∪ 𝑥 ∈ 𝑀 → ∀𝑥 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570  ∃wex 1809   ∈ wcel 2143  ∀wral 3079  ∃wrex 3089  ∪ cuni 4872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-v 3457  df-uni 4873

This theorem is referenced by:  wfaxun  45728