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	$$⊢\bigcup A\in V\to A\in 𝒫𝒫\bigcup V$$

Proof

Step	Hyp	Ref	Expression
1		pwuni	$$⊢A\subseteq 𝒫\bigcup A$$
2		pwel	$$⊢\bigcup A\in V\to 𝒫\bigcup A\in 𝒫𝒫\bigcup V$$
3		bj-sselpwuni	$$⊢\left(A\subseteq 𝒫\bigcup A\wedge 𝒫\bigcup A\in 𝒫𝒫\bigcup V\right)\to A\in 𝒫\bigcup 𝒫𝒫\bigcup V$$
4	1 2 3	sylancr	$$⊢\bigcup A\in V\to A\in 𝒫\bigcup 𝒫𝒫\bigcup V$$
5		unipw	$$⊢\bigcup 𝒫𝒫\bigcup V=𝒫\bigcup V$$
6	5	pweqi	$$⊢𝒫\bigcup 𝒫𝒫\bigcup V=𝒫𝒫\bigcup V$$
7	4 6	eleqtrdi	$$⊢\bigcup A\in V\to A\in 𝒫𝒫\bigcup V$$