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 CVxABCAAFinxABfiC

Proof

Step Hyp Ref Expression
1 simpr1 CVxABCAAFinxABC
2 dfiin2g xABCxAB=y|xAy=B
3 1 2 syl CVxABCAAFinxAB=y|xAy=B
4 eqid xAB=xAB
5 4 rnmpt ranxAB=y|xAy=B
6 5 inteqi ranxAB=y|xAy=B
7 3 6 eqtr4di CVxABCAAFinxAB=ranxAB
8 4 fmpt xABCxAB:AC
9 8 3anbi1i xABCAAFinxAB:ACAAFin
10 intrnfi CVxAB:ACAAFinranxABfiC
11 9 10 sylan2b CVxABCAAFinranxABfiC
12 7 11 eqeltrd CVxABCAAFinxABfiC