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	⊢ ( 𝑍 ∈ 𝑉 → ( 𝑍 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ) )