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	syl5eq	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐼 𝑆 ⊆ 𝑋 ) → ∩ ( { 𝑋 } ∪ ran ( 𝑘 ∈ 𝐼 ↦ 𝑆 ) ) = ( 𝑋 ∩ ∩ ran ( 𝑘 ∈ 𝐼 ↦ 𝑆 ) ) )
13	7 12	eqtr4d	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐼 𝑆 ⊆ 𝑋 ) → ( 𝑋 ∩ ∩ 𝑘 ∈ 𝐼 𝑆 ) = ∩ ( { 𝑋 } ∪ ran ( 𝑘 ∈ 𝐼 ↦ 𝑆 ) ) )