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 ⊢ X ∈ V ∧ ∀ k ∈ I S ⊆ X → X ∩ ⋂ k ∈ I S = ⋂ X ∪ ran ⁡ k ∈ I ⟼ S

Proof

Step Hyp Ref Expression
1 ssexg ⊢ S ⊆ X ∧ X ∈ V → S ∈ V
2 1 expcom ⊢ X ∈ V → S ⊆ X → S ∈ V
3 2 ralimdv ⊢ X ∈ V → ∀ k ∈ I S ⊆ X → ∀ k ∈ I S ∈ V
4 3 imp ⊢ X ∈ V ∧ ∀ k ∈ I S ⊆ X → ∀ k ∈ I S ∈ V
5 dfiin3g ⊢ ∀ k ∈ I S ∈ V → ⋂ k ∈ I S = ⋂ ran ⁡ k ∈ I ⟼ S
6 4 5 syl ⊢ X ∈ V ∧ ∀ k ∈ I S ⊆ X → ⋂ k ∈ I S = ⋂ ran ⁡ k ∈ I ⟼ S
7 6 ineq2d ⊢ X ∈ V ∧ ∀ k ∈ I S ⊆ X → X ∩ ⋂ k ∈ I S = X ∩ ⋂ ran ⁡ k ∈ I ⟼ S
8 intun ⊢ ⋂ X ∪ ran ⁡ k ∈ I ⟼ S = ⋂ X ∩ ⋂ ran ⁡ k ∈ I ⟼ S
9 intsng ⊢ X ∈ V → ⋂ X = X
10 9 adantr ⊢ X ∈ V ∧ ∀ k ∈ I S ⊆ X → ⋂ X = X
11 10 ineq1d ⊢ X ∈ V ∧ ∀ k ∈ I S ⊆ X → ⋂ X ∩ ⋂ ran ⁡ k ∈ I ⟼ S = X ∩ ⋂ ran ⁡ k ∈ I ⟼ S
12 8 11 syl5eq ⊢ X ∈ V ∧ ∀ k ∈ I S ⊆ X → ⋂ X ∪ ran ⁡ k ∈ I ⟼ S = X ∩ ⋂ ran ⁡ k ∈ I ⟼ S
13 7 12 eqtr4d ⊢ X ∈ V ∧ ∀ k ∈ I S ⊆ X → X ∩ ⋂ k ∈ I S = ⋂ X ∪ ran ⁡ k ∈ I ⟼ S