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

Metamath Proof Explorer

Theorem eliuniin2

Description: Indexed union of indexed intersections. See eliincex for a counterexample showing that the precondition C =/= (/) cannot be simply dropped. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses eliuniin2.1 ⊢ Ⅎ 𝑥 𝐶
eliuniin2.2 ⊢ 𝐴 = ∪ 𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷
Assertion eliuniin2 ( 𝐶 ≠ ∅ → ( 𝑍 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 eliuniin2.1 ⊢ Ⅎ 𝑥 𝐶
2 eliuniin2.2 ⊢ 𝐴 = ∪ 𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷
3 2 eleq2i ⊢ ( 𝑍 ∈ 𝐴 ↔ 𝑍 ∈ ∪ 𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷 )
4 eliun ⊢ ( 𝑍 ∈ ∪ 𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷 ↔ ∃ 𝑥 ∈ 𝐵 𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 )
5 3 4 sylbb ⊢ ( 𝑍 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐵 𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 )
6 eliin ⊢ ( 𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 → ( 𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 ↔ ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ) )
7 6 ibi ⊢ ( 𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 → ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 )
8 7 a1i ⊢ ( 𝑍 ∈ 𝐴 → ( 𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 → ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ) )
9 8 reximdv ⊢ ( 𝑍 ∈ 𝐴 → ( ∃ 𝑥 ∈ 𝐵 𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ) )
10 5 9 mpd ⊢ ( 𝑍 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 )
11 nfcv ⊢ Ⅎ 𝑥 ∅
12 1 11 nfne ⊢ Ⅎ 𝑥 𝐶 ≠ ∅
13 nfv ⊢ Ⅎ 𝑥 𝑍 ∈ 𝐴
14 simp2 ⊢ ( ( 𝐶 ≠ ∅ ∧ 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ) → 𝑥 ∈ 𝐵 )
15 eliin2 ⊢ ( 𝐶 ≠ ∅ → ( 𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 ↔ ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ) )
16 15 biimpar ⊢ ( ( 𝐶 ≠ ∅ ∧ ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ) → 𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 )
17 rspe ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 ) → ∃ 𝑥 ∈ 𝐵 𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 )
18 14 16 17 3imp3i2an ⊢ ( ( 𝐶 ≠ ∅ ∧ 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ) → ∃ 𝑥 ∈ 𝐵 𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 )
19 18 4 sylibr ⊢ ( ( 𝐶 ≠ ∅ ∧ 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ) → 𝑍 ∈ ∪ 𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷 )
20 19 3 sylibr ⊢ ( ( 𝐶 ≠ ∅ ∧ 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ) → 𝑍 ∈ 𝐴 )
21 20 3exp ⊢ ( 𝐶 ≠ ∅ → ( 𝑥 ∈ 𝐵 → ( ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 → 𝑍 ∈ 𝐴 ) ) )
22 12 13 21 rexlimd ⊢ ( 𝐶 ≠ ∅ → ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 → 𝑍 ∈ 𝐴 ) )
23 10 22 impbid2 ⊢ ( 𝐶 ≠ ∅ → ( 𝑍 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ) )