Theorem uniclaxun 45430

Description: A class that is closed under the union operation models the Axiom of Union ax-un 7678. 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 3069	. . . . 5 ⊢ (∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))
2		eluni 4841	. . . . 5 ⊢ (𝑧 ∈ ∪ 𝑥 ↔ ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))
3	1, 2	sylibr 235	. . . 4 ⊢ (∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ ∪ 𝑥)
4	3	rgenw 3057	. . 3 ⊢ ∀𝑧 ∈ 𝑀 (∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ ∪ 𝑥)
5		eleq2 2828	. . . . . 6 ⊢ (𝑦 = ∪ 𝑥 → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ ∪ 𝑥))
6	5	imbi2d 341	. . . . 5 ⊢ (𝑦 = ∪ 𝑥 → ((∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ (∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ ∪ 𝑥)))
7	6	ralbidv 3162	. . . 4 ⊢ (𝑦 = ∪ 𝑥 → (∀𝑧 ∈ 𝑀 (∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ∀𝑧 ∈ 𝑀 (∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ ∪ 𝑥)))
8	7	rspcev 3560	. . 3 ⊢ ((∪ 𝑥 ∈ 𝑀 ∧ ∀𝑧 ∈ 𝑀 (∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ ∪ 𝑥)) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))
9	4, 8	mpan2 697	. 2 ⊢ (∪ 𝑥 ∈ 𝑀 → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))
10	9	ralimi 3076	1 ⊢ (∀𝑥 ∈ 𝑀 ∪ 𝑥 ∈ 𝑀 → ∀𝑥 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547  ∃wex 1786   ∈ wcel 2119  ∀wral 3053  ∃wrex 3063  ∪ cuni 4838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-v 3433  df-uni 4839

This theorem is referenced by:  wfaxun  45443