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 V A fi B x 𝒫 B Fin A = x

Proof

Step Hyp Ref Expression
1 elex A fi B A V
2 1 a1i B V A fi B A V
3 simpr x 𝒫 B Fin A = x A = x
4 eldifsni x 𝒫 B Fin x
5 4 adantr x 𝒫 B Fin A = x x
6 intex x x V
7 5 6 sylib x 𝒫 B Fin A = x x V
8 3 7 eqeltrd x 𝒫 B Fin A = x A V
9 8 rexlimiva x 𝒫 B Fin A = x A V
10 9 a1i B V x 𝒫 B Fin A = x A V
11 elfi A V B V A fi B x 𝒫 B Fin A = x
12 vprc ¬ V V
13 elsni x x =
14 13 inteqd x x =
15 int0 = V
16 14 15 eqtrdi x x = V
17 16 eleq1d x x V V V
18 12 17 mtbiri x ¬ x V
19 simpr A V B V A = x A = x
20 simpll A V B V A = x A V
21 19 20 eqeltrrd A V B V A = x x V
22 18 21 nsyl3 A V B V A = x ¬ x
23 22 biantrud A V B V A = x x 𝒫 B Fin x 𝒫 B Fin ¬ x
24 eldif x 𝒫 B Fin x 𝒫 B Fin ¬ x
25 23 24 bitr4di A V B V A = x x 𝒫 B Fin x 𝒫 B Fin
26 25 pm5.32da A V B V A = x x 𝒫 B Fin A = x x 𝒫 B Fin
27 ancom x 𝒫 B Fin A = x A = x x 𝒫 B Fin
28 ancom x 𝒫 B Fin A = x A = x x 𝒫 B Fin
29 26 27 28 3bitr4g A V B V x 𝒫 B Fin A = x x 𝒫 B Fin A = x
30 29 rexbidv2 A V B V x 𝒫 B Fin A = x x 𝒫 B Fin A = x
31 11 30 bitrd A V B V A fi B x 𝒫 B Fin A = x
32 31 expcom B V A V A fi B x 𝒫 B Fin A = x
33 2 10 32 pm5.21ndd B V A fi B x 𝒫 B Fin A = x