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 eqtrdi
 |-  ( 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 bitr4di
 |-  ( ( ( 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 ) )