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

Metamath Proof Explorer

Theorem riinint

Description: Express a relative indexed intersection as an intersection. (Contributed by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Assertion riinint ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐼 𝑆 ⊆ 𝑋 ) → ( 𝑋 ∩ ∩ 𝑘 ∈ 𝐼 𝑆 ) = ∩ ( { 𝑋 } ∪ ran ( 𝑘 ∈ 𝐼 ↦ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 ssexg ⊢ ( ( 𝑆 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) → 𝑆 ∈ V )
2 1 expcom ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑆 ⊆ 𝑋 → 𝑆 ∈ V ) )
3 2 ralimdv ⊢ ( 𝑋 ∈ 𝑉 → ( ∀ 𝑘 ∈ 𝐼 𝑆 ⊆ 𝑋 → ∀ 𝑘 ∈ 𝐼 𝑆 ∈ V ) )
4 3 imp ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐼 𝑆 ⊆ 𝑋 ) → ∀ 𝑘 ∈ 𝐼 𝑆 ∈ V )
5 dfiin3g ⊢ ( ∀ 𝑘 ∈ 𝐼 𝑆 ∈ V → ∩ 𝑘 ∈ 𝐼 𝑆 = ∩ ran ( 𝑘 ∈ 𝐼 ↦ 𝑆 ) )
6 4 5 syl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐼 𝑆 ⊆ 𝑋 ) → ∩ 𝑘 ∈ 𝐼 𝑆 = ∩ ran ( 𝑘 ∈ 𝐼 ↦ 𝑆 ) )
7 6 ineq2d ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐼 𝑆 ⊆ 𝑋 ) → ( 𝑋 ∩ ∩ 𝑘 ∈ 𝐼 𝑆 ) = ( 𝑋 ∩ ∩ ran ( 𝑘 ∈ 𝐼 ↦ 𝑆 ) ) )
8 intun ⊢ ∩ ( { 𝑋 } ∪ ran ( 𝑘 ∈ 𝐼 ↦ 𝑆 ) ) = ( ∩ { 𝑋 } ∩ ∩ ran ( 𝑘 ∈ 𝐼 ↦ 𝑆 ) )
9 intsng ⊢ ( 𝑋 ∈ 𝑉 → ∩ { 𝑋 } = 𝑋 )
10 9 adantr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐼 𝑆 ⊆ 𝑋 ) → ∩ { 𝑋 } = 𝑋 )
11 10 ineq1d ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐼 𝑆 ⊆ 𝑋 ) → ( ∩ { 𝑋 } ∩ ∩ ran ( 𝑘 ∈ 𝐼 ↦ 𝑆 ) ) = ( 𝑋 ∩ ∩ ran ( 𝑘 ∈ 𝐼 ↦ 𝑆 ) ) )
12 8 11 eqtrid ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐼 𝑆 ⊆ 𝑋 ) → ∩ ( { 𝑋 } ∪ ran ( 𝑘 ∈ 𝐼 ↦ 𝑆 ) ) = ( 𝑋 ∩ ∩ ran ( 𝑘 ∈ 𝐼 ↦ 𝑆 ) ) )
13 7 12 eqtr4d ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐼 𝑆 ⊆ 𝑋 ) → ( 𝑋 ∩ ∩ 𝑘 ∈ 𝐼 𝑆 ) = ∩ ( { 𝑋 } ∪ ran ( 𝑘 ∈ 𝐼 ↦ 𝑆 ) ) )