Metamath Proof Explorer

Theorem elfi2

Description: The empty intersection need not be considered in the set of finite intersections. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion elfi2 
|- ( B e. V -> ( A e. ( fi ` B ) <-> E. x e. ( ( ~P B i^i Fin ) \ { (/) } ) A = |^| x ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. ( fi ` B ) -> A e. _V )
2 1 a1i 
 |-  ( B e. V -> ( A e. ( fi ` B ) -> A e. _V ) )
3 simpr 
 |-  ( ( x e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ A = |^| x ) -> A = |^| x )
4 eldifsni 
 |-  ( x e. ( ( ~P B i^i Fin ) \ { (/) } ) -> x =/= (/) )
5 4 adantr 
 |-  ( ( x e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ A = |^| x ) -> x =/= (/) )
6 intex 
 |-  ( x =/= (/) <-> |^| x e. _V )
7 5 6 sylib 
 |-  ( ( x e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ A = |^| x ) -> |^| x e. _V )
8 3 7 eqeltrd 
 |-  ( ( x e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ A = |^| x ) -> A e. _V )
9 8 rexlimiva 
 |-  ( E. x e. ( ( ~P B i^i Fin ) \ { (/) } ) A = |^| x -> A e. _V )
10 9 a1i 
 |-  ( B e. V -> ( E. x e. ( ( ~P B i^i Fin ) \ { (/) } ) A = |^| x -> A e. _V ) )
11 elfi 
 |-  ( ( A e. _V /\ B e. V ) -> ( A e. ( fi ` B ) <-> E. x e. ( ~P B i^i Fin ) A = |^| x ) )
12 vprc 
 |-  -. _V e. _V
13 elsni 
 |-  ( x e. { (/) } -> x = (/) )
14 13 inteqd 
 |-  ( x e. { (/) } -> |^| x = |^| (/) )
15 int0 
 |-  |^| (/) = _V
16 14 15 syl6eq 
 |-  ( x e. { (/) } -> |^| x = _V )
17 16 eleq1d 
 |-  ( x e. { (/) } -> ( |^| x e. _V <-> _V e. _V ) )
18 12 17 mtbiri 
 |-  ( x e. { (/) } -> -. |^| x e. _V )
19 simpr 
 |-  ( ( ( A e. _V /\ B e. V ) /\ A = |^| x ) -> A = |^| x )
20 simpll 
 |-  ( ( ( A e. _V /\ B e. V ) /\ A = |^| x ) -> A e. _V )
21 19 20 eqeltrrd 
 |-  ( ( ( A e. _V /\ B e. V ) /\ A = |^| x ) -> |^| x e. _V )
22 18 21 nsyl3 
 |-  ( ( ( A e. _V /\ B e. V ) /\ A = |^| x ) -> -. x e. { (/) } )
23 22 biantrud 
 |-  ( ( ( A e. _V /\ B e. V ) /\ A = |^| x ) -> ( x e. ( ~P B i^i Fin ) <-> ( x e. ( ~P B i^i Fin ) /\ -. x e. { (/) } ) ) )
24 eldif 
 |-  ( x e. ( ( ~P B i^i Fin ) \ { (/) } ) <-> ( x e. ( ~P B i^i Fin ) /\ -. x e. { (/) } ) )
25 23 24 syl6bbr 
 |-  ( ( ( A e. _V /\ B e. V ) /\ A = |^| x ) -> ( x e. ( ~P B i^i Fin ) <-> x e. ( ( ~P B i^i Fin ) \ { (/) } ) ) )
26 25 pm5.32da 
 |-  ( ( A e. _V /\ B e. V ) -> ( ( A = |^| x /\ x e. ( ~P B i^i Fin ) ) <-> ( A = |^| x /\ x e. ( ( ~P B i^i Fin ) \ { (/) } ) ) ) )
27 ancom 
 |-  ( ( x e. ( ~P B i^i Fin ) /\ A = |^| x ) <-> ( A = |^| x /\ x e. ( ~P B i^i Fin ) ) )
28 ancom 
 |-  ( ( x e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ A = |^| x ) <-> ( A = |^| x /\ x e. ( ( ~P B i^i Fin ) \ { (/) } ) ) )
29 26 27 28 3bitr4g 
 |-  ( ( A e. _V /\ B e. V ) -> ( ( x e. ( ~P B i^i Fin ) /\ A = |^| x ) <-> ( x e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ A = |^| x ) ) )
30 29 rexbidv2 
 |-  ( ( A e. _V /\ B e. V ) -> ( E. x e. ( ~P B i^i Fin ) A = |^| x <-> E. x e. ( ( ~P B i^i Fin ) \ { (/) } ) A = |^| x ) )
31 11 30 bitrd 
 |-  ( ( A e. _V /\ B e. V ) -> ( A e. ( fi ` B ) <-> E. x e. ( ( ~P B i^i Fin ) \ { (/) } ) A = |^| x ) )
32 31 expcom 
 |-  ( B e. V -> ( A e. _V -> ( A e. ( fi ` B ) <-> E. x e. ( ( ~P B i^i Fin ) \ { (/) } ) A = |^| x ) ) )
33 2 10 32 pm5.21ndd 
 |-  ( B e. V -> ( A e. ( fi ` B ) <-> E. x e. ( ( ~P B i^i Fin ) \ { (/) } ) A = |^| x ) )