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

Metamath Proof Explorer

Theorem imaiun

Description: The image of an indexed union is the indexed union of the images. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Assertion imaiun ( 𝐴 “ ∪ 𝑥 ∈ 𝐵 𝐶 ) = ∪ 𝑥 ∈ 𝐵 ( 𝐴 “ 𝐶 )

Proof

Step Hyp Ref Expression
1 rexcom4 ⊢ ( ∃ 𝑥 ∈ 𝐵 ∃ 𝑧 ( 𝑧 ∈ 𝐶 ∧ ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐴 ) ↔ ∃ 𝑧 ∃ 𝑥 ∈ 𝐵 ( 𝑧 ∈ 𝐶 ∧ ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐴 ) )
2 vex ⊢ 𝑦 ∈ V
3 2 elima3 ⊢ ( 𝑦 ∈ ( 𝐴 “ 𝐶 ) ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐶 ∧ ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐴 ) )
4 3 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐵 𝑦 ∈ ( 𝐴 “ 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑧 ( 𝑧 ∈ 𝐶 ∧ ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐴 ) )
5 eliun ⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃ 𝑥 ∈ 𝐵 𝑧 ∈ 𝐶 )
6 5 anbi1i ⊢ ( ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ∧ ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐴 ) ↔ ( ∃ 𝑥 ∈ 𝐵 𝑧 ∈ 𝐶 ∧ ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐴 ) )
7 r19.41v ⊢ ( ∃ 𝑥 ∈ 𝐵 ( 𝑧 ∈ 𝐶 ∧ ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐴 ) ↔ ( ∃ 𝑥 ∈ 𝐵 𝑧 ∈ 𝐶 ∧ ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐴 ) )
8 6 7 bitr4i ⊢ ( ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ∧ ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐵 ( 𝑧 ∈ 𝐶 ∧ ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐴 ) )
9 8 exbii ⊢ ( ∃ 𝑧 ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ∧ ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐴 ) ↔ ∃ 𝑧 ∃ 𝑥 ∈ 𝐵 ( 𝑧 ∈ 𝐶 ∧ ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐴 ) )
10 1 4 9 3bitr4ri ⊢ ( ∃ 𝑧 ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ∧ ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐵 𝑦 ∈ ( 𝐴 “ 𝐶 ) )
11 2 elima3 ⊢ ( 𝑦 ∈ ( 𝐴 “ ∪ 𝑥 ∈ 𝐵 𝐶 ) ↔ ∃ 𝑧 ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ∧ ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐴 ) )
12 eliun ⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 ( 𝐴 “ 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐵 𝑦 ∈ ( 𝐴 “ 𝐶 ) )
13 10 11 12 3bitr4i ⊢ ( 𝑦 ∈ ( 𝐴 “ ∪ 𝑥 ∈ 𝐵 𝐶 ) ↔ 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 ( 𝐴 “ 𝐶 ) )
14 13 eqriv ⊢ ( 𝐴 “ ∪ 𝑥 ∈ 𝐵 𝐶 ) = ∪ 𝑥 ∈ 𝐵 ( 𝐴 “ 𝐶 )