Theorem iinss2d

Description: Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 24-Jan-2025)

	Ref	Expression
Hypotheses	iinss2d.1	⊢ Ⅎ 𝑥 𝜑
	iinss2d.2	⊢ Ⅎ 𝑥 𝐴
	iinss2d.3	⊢ Ⅎ 𝑥 𝐶
	iinss2d.4	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
	iinss2d.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ⊆ 𝐶 )
Assertion	iinss2d	⊢ ( 𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		iinss2d.1	⊢ Ⅎ 𝑥 𝜑
2		iinss2d.2	⊢ Ⅎ 𝑥 𝐴
3		iinss2d.3	⊢ Ⅎ 𝑥 𝐶
4		iinss2d.4	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
5		iinss2d.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ⊆ 𝐶 )
6	5	3adant3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ⊤ ) → 𝐵 ⊆ 𝐶 )
7	2	n0f	⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
8	4 7	sylib	⊢ ( 𝜑 → ∃ 𝑥 𝑥 ∈ 𝐴 )
9		rextru	⊢ ( ∃ 𝑥 𝑥 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ⊤ )
10	8 9	sylib	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ⊤ )
11	1 6 10	reximdd	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 )
12	3	iinssf	⊢ ( ∃ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 )
13	11 12	syl	⊢ ( 𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 )