Theorem elpwiuncl

Description: Closure of indexed union with regard to elementhood to a power set. (Contributed by Thierry Arnoux, 27-May-2020)

	Ref	Expression
Hypotheses	elpwiuncl.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	elpwiuncl.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝒫 𝐶 )
Assertion	elpwiuncl	⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ 𝒫 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		elpwiuncl.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		elpwiuncl.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝒫 𝐶 )
3	2	elpwid	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ⊆ 𝐶 )
4	3	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐵 ⊆ 𝐶 )
5		iunss	⊢ ( ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀ 𝑘 ∈ 𝐴 𝐵 ⊆ 𝐶 )
6	4 5	sylibr	⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ 𝐶 )
7	2	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ 𝒫 𝐶 )
8	1 7	jca	⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ 𝒫 𝐶 ) )
9		iunexg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ 𝒫 𝐶 ) → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ V )
10		elpwg	⊢ ( ∪ 𝑘 ∈ 𝐴 𝐵 ∈ V → ( ∪ 𝑘 ∈ 𝐴 𝐵 ∈ 𝒫 𝐶 ↔ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ 𝐶 ) )
11	8 9 10	3syl	⊢ ( 𝜑 → ( ∪ 𝑘 ∈ 𝐴 𝐵 ∈ 𝒫 𝐶 ↔ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ 𝐶 ) )
12	6 11	mpbird	⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ 𝒫 𝐶 )