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 ( 𝐶 ≠ ∅ → ( 𝑍𝐴 ↔ ∃ 𝑥𝐵𝑦𝐶 𝑍𝐷 ) )