Theorem bj-unirel

Description: Quantitative version of uniexr : if the union of a class is an element of a class, then that class is an element of the double powerclass of the union of this class. (Contributed by BJ, 6-Apr-2024)

	Ref	Expression
Assertion	bj-unirel	⊢ ( ∪ 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝒫 ∪ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		pwuni	⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴
2		pwel	⊢ ( ∪ 𝐴 ∈ 𝑉 → 𝒫 ∪ 𝐴 ∈ 𝒫 𝒫 ∪ 𝑉 )
3		bj-sselpwuni	⊢ ( ( 𝐴 ⊆ 𝒫 ∪ 𝐴 ∧ 𝒫 ∪ 𝐴 ∈ 𝒫 𝒫 ∪ 𝑉 ) → 𝐴 ∈ 𝒫 ∪ 𝒫 𝒫 ∪ 𝑉 )
4	1 2 3	sylancr	⊢ ( ∪ 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 ∪ 𝒫 𝒫 ∪ 𝑉 )
5		unipw	⊢ ∪ 𝒫 𝒫 ∪ 𝑉 = 𝒫 ∪ 𝑉
6	5	pweqi	⊢ 𝒫 ∪ 𝒫 𝒫 ∪ 𝑉 = 𝒫 𝒫 ∪ 𝑉
7	4 6	eleqtrdi	⊢ ( ∪ 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝒫 ∪ 𝑉 )