Theorem iinfi

Description: An indexed intersection of elements of C is an element of the finite intersections of C . (Contributed by Mario Carneiro, 30-Aug-2015)

	Ref	Expression
Assertion	iinfi	⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ ( fi ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		simpr1	⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 )
2		dfiin2g	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )
3	1 2	syl	⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )
4		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
5	4	rnmpt	⊢ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 }
6	5	inteqi	⊢ ∩ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 }
7	3 6	eqtr4di	⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
8	4	fmpt	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝐶 )
9	8	3anbi1i	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝐶 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) )
10		intrnfi	⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝐶 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → ∩ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( fi ‘ 𝐶 ) )
11	9 10	sylan2b	⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → ∩ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( fi ‘ 𝐶 ) )
12	7 11	eqeltrd	⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ ( fi ‘ 𝐶 ) )