Metamath Proof Explorer

Theorem elrfirn2

Description: Elementhood in a set of relative finite intersections of an indexed family of sets (implicit). (Contributed by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Assertion elrfirn2 
|- ( ( B e. V /\ A. y e. I C C_ B ) -> ( A e. ( fi ` ( { B } u. ran ( y e. I |-> C ) ) ) <-> E. v e. ( ~P I i^i Fin ) A = ( B i^i |^|_ y e. v C ) ) )

Proof

Step Hyp Ref Expression
1 elpw2g 
 |-  ( B e. V -> ( C e. ~P B <-> C C_ B ) )
2 1 biimprd 
 |-  ( B e. V -> ( C C_ B -> C e. ~P B ) )
3 2 ralimdv 
 |-  ( B e. V -> ( A. y e. I C C_ B -> A. y e. I C e. ~P B ) )
4 3 imp 
 |-  ( ( B e. V /\ A. y e. I C C_ B ) -> A. y e. I C e. ~P B )
5 eqid 
 |-  ( y e. I |-> C ) = ( y e. I |-> C )
6 5 fmpt 
 |-  ( A. y e. I C e. ~P B <-> ( y e. I |-> C ) : I --> ~P B )
7 4 6 sylib 
 |-  ( ( B e. V /\ A. y e. I C C_ B ) -> ( y e. I |-> C ) : I --> ~P B )
8 elrfirn 
 |-  ( ( B e. V /\ ( y e. I |-> C ) : I --> ~P B ) -> ( A e. ( fi ` ( { B } u. ran ( y e. I |-> C ) ) ) <-> E. v e. ( ~P I i^i Fin ) A = ( B i^i |^|_ z e. v ( ( y e. I |-> C ) ` z ) ) ) )
9 7 8 syldan 
 |-  ( ( B e. V /\ A. y e. I C C_ B ) -> ( A e. ( fi ` ( { B } u. ran ( y e. I |-> C ) ) ) <-> E. v e. ( ~P I i^i Fin ) A = ( B i^i |^|_ z e. v ( ( y e. I |-> C ) ` z ) ) ) )
10 inss1 
 |-  ( ~P I i^i Fin ) C_ ~P I
11 10 sseli 
 |-  ( v e. ( ~P I i^i Fin ) -> v e. ~P I )
12 11 elpwid 
 |-  ( v e. ( ~P I i^i Fin ) -> v C_ I )
13 nffvmpt1 
 |-  F/_ y ( ( y e. I |-> C ) ` z )
14 nfcv 
 |-  F/_ z ( ( y e. I |-> C ) ` y )
15 fveq2 
 |-  ( z = y -> ( ( y e. I |-> C ) ` z ) = ( ( y e. I |-> C ) ` y ) )
16 13 14 15 cbviin 
 |-  |^|_ z e. v ( ( y e. I |-> C ) ` z ) = |^|_ y e. v ( ( y e. I |-> C ) ` y )
17 simplr 
 |-  ( ( ( B e. V /\ y e. I ) /\ C C_ B ) -> y e. I )
18 simpll 
 |-  ( ( ( B e. V /\ y e. I ) /\ C C_ B ) -> B e. V )
19 simpr 
 |-  ( ( ( B e. V /\ y e. I ) /\ C C_ B ) -> C C_ B )
20 18 19 ssexd 
 |-  ( ( ( B e. V /\ y e. I ) /\ C C_ B ) -> C e. _V )
21 5 fvmpt2 
 |-  ( ( y e. I /\ C e. _V ) -> ( ( y e. I |-> C ) ` y ) = C )
22 17 20 21 syl2anc 
 |-  ( ( ( B e. V /\ y e. I ) /\ C C_ B ) -> ( ( y e. I |-> C ) ` y ) = C )
23 22 ex 
 |-  ( ( B e. V /\ y e. I ) -> ( C C_ B -> ( ( y e. I |-> C ) ` y ) = C ) )
24 23 ralimdva 
 |-  ( B e. V -> ( A. y e. I C C_ B -> A. y e. I ( ( y e. I |-> C ) ` y ) = C ) )
25 24 imp 
 |-  ( ( B e. V /\ A. y e. I C C_ B ) -> A. y e. I ( ( y e. I |-> C ) ` y ) = C )
26 ssralv 
 |-  ( v C_ I -> ( A. y e. I ( ( y e. I |-> C ) ` y ) = C -> A. y e. v ( ( y e. I |-> C ) ` y ) = C ) )
27 25 26 mpan9 
 |-  ( ( ( B e. V /\ A. y e. I C C_ B ) /\ v C_ I ) -> A. y e. v ( ( y e. I |-> C ) ` y ) = C )
28 iineq2 
 |-  ( A. y e. v ( ( y e. I |-> C ) ` y ) = C -> |^|_ y e. v ( ( y e. I |-> C ) ` y ) = |^|_ y e. v C )
29 27 28 syl 
 |-  ( ( ( B e. V /\ A. y e. I C C_ B ) /\ v C_ I ) -> |^|_ y e. v ( ( y e. I |-> C ) ` y ) = |^|_ y e. v C )
30 16 29 syl5eq 
 |-  ( ( ( B e. V /\ A. y e. I C C_ B ) /\ v C_ I ) -> |^|_ z e. v ( ( y e. I |-> C ) ` z ) = |^|_ y e. v C )
31 30 ineq2d 
 |-  ( ( ( B e. V /\ A. y e. I C C_ B ) /\ v C_ I ) -> ( B i^i |^|_ z e. v ( ( y e. I |-> C ) ` z ) ) = ( B i^i |^|_ y e. v C ) )
32 31 eqeq2d 
 |-  ( ( ( B e. V /\ A. y e. I C C_ B ) /\ v C_ I ) -> ( A = ( B i^i |^|_ z e. v ( ( y e. I |-> C ) ` z ) ) <-> A = ( B i^i |^|_ y e. v C ) ) )
33 12 32 sylan2 
 |-  ( ( ( B e. V /\ A. y e. I C C_ B ) /\ v e. ( ~P I i^i Fin ) ) -> ( A = ( B i^i |^|_ z e. v ( ( y e. I |-> C ) ` z ) ) <-> A = ( B i^i |^|_ y e. v C ) ) )
34 33 rexbidva 
 |-  ( ( B e. V /\ A. y e. I C C_ B ) -> ( E. v e. ( ~P I i^i Fin ) A = ( B i^i |^|_ z e. v ( ( y e. I |-> C ) ` z ) ) <-> E. v e. ( ~P I i^i Fin ) A = ( B i^i |^|_ y e. v C ) ) )
35 9 34 bitrd 
 |-  ( ( B e. V /\ A. y e. I C C_ B ) -> ( A e. ( fi ` ( { B } u. ran ( y e. I |-> C ) ) ) <-> E. v e. ( ~P I i^i Fin ) A = ( B i^i |^|_ y e. v C ) ) )