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

Metamath Proof Explorer

Theorem eliuniin

Description: Indexed union of indexed intersections. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypothesis eliuniin.1 ⊢ 𝐴 = ∪ 𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷
Assertion eliuniin ( 𝑍 ∈ 𝑉 → ( 𝑍 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 eliuniin.1 ⊢ 𝐴 = ∪ 𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷
2 1 eleq2i ⊢ ( 𝑍 ∈ 𝐴 ↔ 𝑍 ∈ ∪ 𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷 )
3 eliun ⊢ ( 𝑍 ∈ ∪ 𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷 ↔ ∃ 𝑥 ∈ 𝐵 𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 )
4 2 3 sylbb ⊢ ( 𝑍 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐵 𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 )
5 eliin ⊢ ( 𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 → ( 𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 ↔ ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ) )
6 5 ibi ⊢ ( 𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 → ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 )
7 6 a1i ⊢ ( 𝑍 ∈ 𝐴 → ( 𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 → ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ) )
8 7 reximdv ⊢ ( 𝑍 ∈ 𝐴 → ( ∃ 𝑥 ∈ 𝐵 𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ) )
9 4 8 mpd ⊢ ( 𝑍 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 )
10 simp2 ⊢ ( ( 𝑍 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ) → 𝑥 ∈ 𝐵 )
11 eliin ⊢ ( 𝑍 ∈ 𝑉 → ( 𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 ↔ ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ) )
12 11 biimpar ⊢ ( ( 𝑍 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ) → 𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 )
13 rspe ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 ) → ∃ 𝑥 ∈ 𝐵 𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 )
14 10 12 13 3imp3i2an ⊢ ( ( 𝑍 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ) → ∃ 𝑥 ∈ 𝐵 𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 )
15 14 3 sylibr ⊢ ( ( 𝑍 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ) → 𝑍 ∈ ∪ 𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷 )
16 15 2 sylibr ⊢ ( ( 𝑍 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ) → 𝑍 ∈ 𝐴 )
17 16 rexlimdv3a ⊢ ( 𝑍 ∈ 𝑉 → ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 → 𝑍 ∈ 𝐴 ) )
18 9 17 impbid2 ⊢ ( 𝑍 ∈ 𝑉 → ( 𝑍 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ) )