This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ 𝒫 𝐶 )