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
|- ( ( C e. V /\ ( A. x e. A B e. C /\ A =/= (/) /\ A e. Fin ) ) -> |^|_ x e. A B e. ( fi ` C ) )

Proof

Step Hyp Ref Expression
1 simpr1
 |-  ( ( C e. V /\ ( A. x e. A B e. C /\ A =/= (/) /\ A e. Fin ) ) -> A. x e. A B e. C )
2 dfiin2g
 |-  ( A. x e. A B e. C -> |^|_ x e. A B = |^| { y | E. x e. A y = B } )
3 1 2 syl
 |-  ( ( C e. V /\ ( A. x e. A B e. C /\ A =/= (/) /\ A e. Fin ) ) -> |^|_ x e. A B = |^| { y | E. x e. A y = B } )
4 eqid
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
5 4 rnmpt
 |-  ran ( x e. A |-> B ) = { y | E. x e. A y = B }
6 5 inteqi
 |-  |^| ran ( x e. A |-> B ) = |^| { y | E. x e. A y = B }
7 3 6 eqtr4di
 |-  ( ( C e. V /\ ( A. x e. A B e. C /\ A =/= (/) /\ A e. Fin ) ) -> |^|_ x e. A B = |^| ran ( x e. A |-> B ) )
8 4 fmpt
 |-  ( A. x e. A B e. C <-> ( x e. A |-> B ) : A --> C )
9 8 3anbi1i
 |-  ( ( A. x e. A B e. C /\ A =/= (/) /\ A e. Fin ) <-> ( ( x e. A |-> B ) : A --> C /\ A =/= (/) /\ A e. Fin ) )
10 intrnfi
 |-  ( ( C e. V /\ ( ( x e. A |-> B ) : A --> C /\ A =/= (/) /\ A e. Fin ) ) -> |^| ran ( x e. A |-> B ) e. ( fi ` C ) )
11 9 10 sylan2b
 |-  ( ( C e. V /\ ( A. x e. A B e. C /\ A =/= (/) /\ A e. Fin ) ) -> |^| ran ( x e. A |-> B ) e. ( fi ` C ) )
12 7 11 eqeltrd
 |-  ( ( C e. V /\ ( A. x e. A B e. C /\ A =/= (/) /\ A e. Fin ) ) -> |^|_ x e. A B e. ( fi ` C ) )