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	⊢ ( ∀ 𝑥 ∈ 𝑀 ∪ 𝑥 ∈ 𝑀 → ∀ 𝑥 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∃ 𝑤 ∈ 𝑀 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		rexex	⊢ ( ∃ 𝑤 ∈ 𝑀 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) )
2		eluni	⊢ ( 𝑧 ∈ ∪ 𝑥 ↔ ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) )
3	1 2	sylibr	⊢ ( ∃ 𝑤 ∈ 𝑀 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ ∪ 𝑥 )
4	3	rgenw	⊢ ∀ 𝑧 ∈ 𝑀 ( ∃ 𝑤 ∈ 𝑀 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ ∪ 𝑥 )
5		eleq2	⊢ ( 𝑦 = ∪ 𝑥 → ( 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ ∪ 𝑥 ) )
6	5	imbi2d	⊢ ( 𝑦 = ∪ 𝑥 → ( ( ∃ 𝑤 ∈ 𝑀 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ↔ ( ∃ 𝑤 ∈ 𝑀 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ ∪ 𝑥 ) ) )
7	6	ralbidv	⊢ ( 𝑦 = ∪ 𝑥 → ( ∀ 𝑧 ∈ 𝑀 ( ∃ 𝑤 ∈ 𝑀 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ↔ ∀ 𝑧 ∈ 𝑀 ( ∃ 𝑤 ∈ 𝑀 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ ∪ 𝑥 ) ) )
8	7	rspcev	⊢ ( ( ∪ 𝑥 ∈ 𝑀 ∧ ∀ 𝑧 ∈ 𝑀 ( ∃ 𝑤 ∈ 𝑀 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ ∪ 𝑥 ) ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∃ 𝑤 ∈ 𝑀 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )
9	4 8	mpan2	⊢ ( ∪ 𝑥 ∈ 𝑀 → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∃ 𝑤 ∈ 𝑀 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )
10	9	ralimi	⊢ ( ∀ 𝑥 ∈ 𝑀 ∪ 𝑥 ∈ 𝑀 → ∀ 𝑥 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∃ 𝑤 ∈ 𝑀 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )