Theorem uniclaxun 46115

Description: A class that is closed under the union operation models the Axiom of Union ax-un 7758. 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 4872	. . . . 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 3579	. . 3 ⊢ ((∪ 𝑥 ∈ 𝑀 ∧ ∀𝑧 ∈ 𝑀 (∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ ∪ 𝑥)) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))
9	4, 8	mpan2 704	. 2 ⊢ (∪ 𝑥 ∈ 𝑀 → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))
10	9	ralimi 3102	1 ⊢ (∀𝑥 ∈ 𝑀 ∪ 𝑥 ∈ 𝑀 → ∀𝑥 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569  ∃wex 1811   ∈ wcel 2146  ∀wral 3079  ∃wrex 3089  ∪ cuni 4869

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-v 3455  df-uni 4870

This theorem is used by:  wfaxun  46128