Metamath Proof Explorer

Theorem iinssdf

Description: Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses iinssdf.a ⊢ Ⅎ 𝑥 𝐴
iinssdf.n ⊢ Ⅎ 𝑥 𝑋
iinssdf.c ⊢ Ⅎ 𝑥 𝐶
iinssdf.d ⊢ Ⅎ 𝑥 𝐷
iinssdf.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
iinssdf.b ⊢ ( 𝑥 = 𝑋 → 𝐵 = 𝐷 )
iinssdf.s ⊢ ( 𝜑 → 𝐷 ⊆ 𝐶 )
Assertion iinssdf ( 𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 )

Proof

Step Hyp Ref Expression
1 iinssdf.a ⊢ Ⅎ 𝑥 𝐴
2 iinssdf.n ⊢ Ⅎ 𝑥 𝑋
3 iinssdf.c ⊢ Ⅎ 𝑥 𝐶
4 iinssdf.d ⊢ Ⅎ 𝑥 𝐷
5 iinssdf.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
6 iinssdf.b ⊢ ( 𝑥 = 𝑋 → 𝐵 = 𝐷 )
7 iinssdf.s ⊢ ( 𝜑 → 𝐷 ⊆ 𝐶 )
8 4 3 nfss ⊢ Ⅎ 𝑥 𝐷 ⊆ 𝐶
9 6 sseq1d ⊢ ( 𝑥 = 𝑋 → ( 𝐵 ⊆ 𝐶 ↔ 𝐷 ⊆ 𝐶 ) )
10 8 2 1 9 rspcef ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐷 ⊆ 𝐶 ) → ∃ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 )
11 5 7 10 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 )
12 3 iinssf ⊢ ( ∃ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 )
13 11 12 syl ⊢ ( 𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 )