This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iinssiin

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

Ref Expression
Hypotheses iinssiin.1 ⊢ Ⅎ 𝑥 𝜑
iinssiin.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ⊆ 𝐶 )
Assertion iinssiin ( 𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ ∩ 𝑥 ∈ 𝐴 𝐶 )

Proof

Step Hyp Ref Expression
1 iinssiin.1 ⊢ Ⅎ 𝑥 𝜑
2 iinssiin.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ⊆ 𝐶 )
3 nfii1 ⊢ Ⅎ 𝑥 ∩ 𝑥 ∈ 𝐴 𝐵
4 3 nfcri ⊢ Ⅎ 𝑥 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵
5 1 4 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 )
6 2 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ⊆ 𝐶 )
7 eliinid ⊢ ( ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 )
8 7 adantll ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 )
9 6 8 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐶 )
10 9 ex ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ) → ( 𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐶 ) )
11 5 10 ralrimi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ) → ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 )
12 eliin ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ) )
13 12 elv ⊢ ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 )
14 11 13 sylibr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ) → 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐶 )
15 14 ssd ⊢ ( 𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ ∩ 𝑥 ∈ 𝐴 𝐶 )