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