Metamath Proof Explorer


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 ‘ 𝐶 ) )