Metamath Proof Explorer

Theorem elrfirn

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

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

Proof

Step Hyp Ref Expression
1 frn 
 |-  ( F : I --> ~P B -> ran F C_ ~P B )
2 elrfi 
 |-  ( ( B e. V /\ ran F C_ ~P B ) -> ( A e. ( fi ` ( { B } u. ran F ) ) <-> E. w e. ( ~P ran F i^i Fin ) A = ( B i^i |^| w ) ) )
3 1 2 sylan2 
 |-  ( ( B e. V /\ F : I --> ~P B ) -> ( A e. ( fi ` ( { B } u. ran F ) ) <-> E. w e. ( ~P ran F i^i Fin ) A = ( B i^i |^| w ) ) )
4 imassrn 
 |-  ( F " v ) C_ ran F
5 pwexg 
 |-  ( B e. V -> ~P B e. _V )
6 ssexg 
 |-  ( ( ran F C_ ~P B /\ ~P B e. _V ) -> ran F e. _V )
7 1 5 6 syl2anr 
 |-  ( ( B e. V /\ F : I --> ~P B ) -> ran F e. _V )
8 elpw2g 
 |-  ( ran F e. _V -> ( ( F " v ) e. ~P ran F <-> ( F " v ) C_ ran F ) )
9 7 8 syl 
 |-  ( ( B e. V /\ F : I --> ~P B ) -> ( ( F " v ) e. ~P ran F <-> ( F " v ) C_ ran F ) )
10 4 9 mpbiri 
 |-  ( ( B e. V /\ F : I --> ~P B ) -> ( F " v ) e. ~P ran F )
11 10 adantr 
 |-  ( ( ( B e. V /\ F : I --> ~P B ) /\ v e. ( ~P I i^i Fin ) ) -> ( F " v ) e. ~P ran F )
12 ffun 
 |-  ( F : I --> ~P B -> Fun F )
13 12 ad2antlr 
 |-  ( ( ( B e. V /\ F : I --> ~P B ) /\ v e. ( ~P I i^i Fin ) ) -> Fun F )
14 inss2 
 |-  ( ~P I i^i Fin ) C_ Fin
15 14 sseli 
 |-  ( v e. ( ~P I i^i Fin ) -> v e. Fin )
16 15 adantl 
 |-  ( ( ( B e. V /\ F : I --> ~P B ) /\ v e. ( ~P I i^i Fin ) ) -> v e. Fin )
17 imafi 
 |-  ( ( Fun F /\ v e. Fin ) -> ( F " v ) e. Fin )
18 13 16 17 syl2anc 
 |-  ( ( ( B e. V /\ F : I --> ~P B ) /\ v e. ( ~P I i^i Fin ) ) -> ( F " v ) e. Fin )
19 11 18 elind 
 |-  ( ( ( B e. V /\ F : I --> ~P B ) /\ v e. ( ~P I i^i Fin ) ) -> ( F " v ) e. ( ~P ran F i^i Fin ) )
20 ffn 
 |-  ( F : I --> ~P B -> F Fn I )
21 20 ad2antlr 
 |-  ( ( ( B e. V /\ F : I --> ~P B ) /\ w e. ( ~P ran F i^i Fin ) ) -> F Fn I )
22 inss1 
 |-  ( ~P ran F i^i Fin ) C_ ~P ran F
23 22 sseli 
 |-  ( w e. ( ~P ran F i^i Fin ) -> w e. ~P ran F )
24 23 elpwid 
 |-  ( w e. ( ~P ran F i^i Fin ) -> w C_ ran F )
25 24 adantl 
 |-  ( ( ( B e. V /\ F : I --> ~P B ) /\ w e. ( ~P ran F i^i Fin ) ) -> w C_ ran F )
26 inss2 
 |-  ( ~P ran F i^i Fin ) C_ Fin
27 26 sseli 
 |-  ( w e. ( ~P ran F i^i Fin ) -> w e. Fin )
28 27 adantl 
 |-  ( ( ( B e. V /\ F : I --> ~P B ) /\ w e. ( ~P ran F i^i Fin ) ) -> w e. Fin )
29 fipreima 
 |-  ( ( F Fn I /\ w C_ ran F /\ w e. Fin ) -> E. v e. ( ~P I i^i Fin ) ( F " v ) = w )
30 21 25 28 29 syl3anc 
 |-  ( ( ( B e. V /\ F : I --> ~P B ) /\ w e. ( ~P ran F i^i Fin ) ) -> E. v e. ( ~P I i^i Fin ) ( F " v ) = w )
31 eqcom 
 |-  ( ( F " v ) = w <-> w = ( F " v ) )
32 31 rexbii 
 |-  ( E. v e. ( ~P I i^i Fin ) ( F " v ) = w <-> E. v e. ( ~P I i^i Fin ) w = ( F " v ) )
33 30 32 sylib 
 |-  ( ( ( B e. V /\ F : I --> ~P B ) /\ w e. ( ~P ran F i^i Fin ) ) -> E. v e. ( ~P I i^i Fin ) w = ( F " v ) )
34 inteq 
 |-  ( w = ( F " v ) -> |^| w = |^| ( F " v ) )
35 34 ineq2d 
 |-  ( w = ( F " v ) -> ( B i^i |^| w ) = ( B i^i |^| ( F " v ) ) )
36 35 eqeq2d 
 |-  ( w = ( F " v ) -> ( A = ( B i^i |^| w ) <-> A = ( B i^i |^| ( F " v ) ) ) )
37 36 adantl 
 |-  ( ( ( B e. V /\ F : I --> ~P B ) /\ w = ( F " v ) ) -> ( A = ( B i^i |^| w ) <-> A = ( B i^i |^| ( F " v ) ) ) )
38 19 33 37 rexxfrd 
 |-  ( ( B e. V /\ F : I --> ~P B ) -> ( E. w e. ( ~P ran F i^i Fin ) A = ( B i^i |^| w ) <-> E. v e. ( ~P I i^i Fin ) A = ( B i^i |^| ( F " v ) ) ) )
39 20 ad2antlr 
 |-  ( ( ( B e. V /\ F : I --> ~P B ) /\ v e. ( ~P I i^i Fin ) ) -> F Fn I )
40 inss1 
 |-  ( ~P I i^i Fin ) C_ ~P I
41 40 sseli 
 |-  ( v e. ( ~P I i^i Fin ) -> v e. ~P I )
42 41 elpwid 
 |-  ( v e. ( ~P I i^i Fin ) -> v C_ I )
43 42 adantl 
 |-  ( ( ( B e. V /\ F : I --> ~P B ) /\ v e. ( ~P I i^i Fin ) ) -> v C_ I )
44 imaiinfv 
 |-  ( ( F Fn I /\ v C_ I ) -> |^|_ y e. v ( F ` y ) = |^| ( F " v ) )
45 39 43 44 syl2anc 
 |-  ( ( ( B e. V /\ F : I --> ~P B ) /\ v e. ( ~P I i^i Fin ) ) -> |^|_ y e. v ( F ` y ) = |^| ( F " v ) )
46 45 eqcomd 
 |-  ( ( ( B e. V /\ F : I --> ~P B ) /\ v e. ( ~P I i^i Fin ) ) -> |^| ( F " v ) = |^|_ y e. v ( F ` y ) )
47 46 ineq2d 
 |-  ( ( ( B e. V /\ F : I --> ~P B ) /\ v e. ( ~P I i^i Fin ) ) -> ( B i^i |^| ( F " v ) ) = ( B i^i |^|_ y e. v ( F ` y ) ) )
48 47 eqeq2d 
 |-  ( ( ( B e. V /\ F : I --> ~P B ) /\ v e. ( ~P I i^i Fin ) ) -> ( A = ( B i^i |^| ( F " v ) ) <-> A = ( B i^i |^|_ y e. v ( F ` y ) ) ) )
49 48 rexbidva 
 |-  ( ( B e. V /\ F : I --> ~P B ) -> ( E. v e. ( ~P I i^i Fin ) A = ( B i^i |^| ( F " v ) ) <-> E. v e. ( ~P I i^i Fin ) A = ( B i^i |^|_ y e. v ( F ` y ) ) ) )
50 3 38 49 3bitrd 
 |-  ( ( B e. V /\ F : I --> ~P B ) -> ( A e. ( fi ` ( { B } u. ran F ) ) <-> E. v e. ( ~P I i^i Fin ) A = ( B i^i |^|_ y e. v ( F ` y ) ) ) )