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

Metamath Proof Explorer

Theorem riinn0

Description: Relative intersection of a nonempty family. (Contributed by Stefan O'Rear, 3-Apr-2015)

Ref Expression
Assertion riinn0 ( ( ∀ 𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 ∧ 𝑋 ≠ ∅ ) → ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆 ) = ∩ 𝑥 ∈ 𝑋 𝑆 )

Proof

Step Hyp Ref Expression
1 incom ⊢ ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆 ) = ( ∩ 𝑥 ∈ 𝑋 𝑆 ∩ 𝐴 )
2 r19.2z ⊢ ( ( 𝑋 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 ) → ∃ 𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 )
3 2 ancoms ⊢ ( ( ∀ 𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 ∧ 𝑋 ≠ ∅ ) → ∃ 𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 )
4 iinss ⊢ ( ∃ 𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 → ∩ 𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 )
5 3 4 syl ⊢ ( ( ∀ 𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 ∧ 𝑋 ≠ ∅ ) → ∩ 𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 )
6 dfss2 ⊢ ( ∩ 𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 ↔ ( ∩ 𝑥 ∈ 𝑋 𝑆 ∩ 𝐴 ) = ∩ 𝑥 ∈ 𝑋 𝑆 )
7 5 6 sylib ⊢ ( ( ∀ 𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 ∧ 𝑋 ≠ ∅ ) → ( ∩ 𝑥 ∈ 𝑋 𝑆 ∩ 𝐴 ) = ∩ 𝑥 ∈ 𝑋 𝑆 )
8 1 7 eqtrid ⊢ ( ( ∀ 𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 ∧ 𝑋 ≠ ∅ ) → ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆 ) = ∩ 𝑥 ∈ 𝑋 𝑆 )