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 ⊢ φ → A ∈ V
elpwiuncl.2 ⊢ φ ∧ k ∈ A → B ∈ 𝒫 C
Assertion elpwiuncl ⊢ φ → ⋃ k ∈ A B ∈ 𝒫 C

Proof

Step Hyp Ref Expression
1 elpwiuncl.1 ⊢ φ → A ∈ V
2 elpwiuncl.2 ⊢ φ ∧ k ∈ A → B ∈ 𝒫 C
3 2 elpwid ⊢ φ ∧ k ∈ A → B ⊆ C
4 3 ralrimiva ⊢ φ → ∀ k ∈ A B ⊆ C
5 iunss ⊢ ⋃ k ∈ A B ⊆ C ↔ ∀ k ∈ A B ⊆ C
6 4 5 sylibr ⊢ φ → ⋃ k ∈ A B ⊆ C
7 2 ralrimiva ⊢ φ → ∀ k ∈ A B ∈ 𝒫 C
8 1 7 jca ⊢ φ → A ∈ V ∧ ∀ k ∈ A B ∈ 𝒫 C
9 iunexg ⊢ A ∈ V ∧ ∀ k ∈ A B ∈ 𝒫 C → ⋃ k ∈ A B ∈ V
10 elpwg ⊢ ⋃ k ∈ A B ∈ V → ⋃ k ∈ A B ∈ 𝒫 C ↔ ⋃ k ∈ A B ⊆ C
11 8 9 10 3syl ⊢ φ → ⋃ k ∈ A B ∈ 𝒫 C ↔ ⋃ k ∈ A B ⊆ C
12 6 11 mpbird ⊢ φ → ⋃ k ∈ A B ∈ 𝒫 C