Theorem iinssiun

Description: An indexed intersection is a subset of the corresponding indexed union. (Contributed by Thierry Arnoux, 31-Dec-2021)

	Ref	Expression
Assertion	iinssiun	⊢ ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		r19.2z	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
2	1	ex	⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) )
3		eliin	⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) )
4	3	elv	⊢ ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
5		eliun	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
6	2 4 5	3imtr4g	⊢ ( 𝐴 ≠ ∅ → ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
7	6	ssrdv	⊢ ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )