Theorem pwuncl

Description: Power classes are closed under union. (Contributed by AV, 27-Feb-2024)

	Ref	Expression
Assertion	pwuncl	⊢ ( ( 𝐴 ∈ 𝒫 𝑋 ∧ 𝐵 ∈ 𝒫 𝑋 ) → ( 𝐴 ∪ 𝐵 ) ∈ 𝒫 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		unexg	⊢ ( ( 𝐴 ∈ 𝒫 𝑋 ∧ 𝐵 ∈ 𝒫 𝑋 ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
2		elpwi	⊢ ( 𝐴 ∈ 𝒫 𝑋 → 𝐴 ⊆ 𝑋 )
3		elpwi	⊢ ( 𝐵 ∈ 𝒫 𝑋 → 𝐵 ⊆ 𝑋 )
4		unss	⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) ↔ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑋 )
5	4	biimpi	⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( 𝐴 ∪ 𝐵 ) ⊆ 𝑋 )
6	2 3 5	syl2an	⊢ ( ( 𝐴 ∈ 𝒫 𝑋 ∧ 𝐵 ∈ 𝒫 𝑋 ) → ( 𝐴 ∪ 𝐵 ) ⊆ 𝑋 )
7	1 6	elpwd	⊢ ( ( 𝐴 ∈ 𝒫 𝑋 ∧ 𝐵 ∈ 𝒫 𝑋 ) → ( 𝐴 ∪ 𝐵 ) ∈ 𝒫 𝑋 )