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