Metamath Proof Explorer


Theorem fi0

Description: The set of finite intersections of the empty set. (Contributed by Mario Carneiro, 30-Aug-2015)

Ref Expression
Assertion fi0 fi =

Proof

Step Hyp Ref Expression
1 0ex V
2 fival V fi = y | x 𝒫 Fin y = x
3 1 2 ax-mp fi = y | x 𝒫 Fin y = x
4 vprc ¬ V V
5 id y = x y = x
6 elinel1 x 𝒫 Fin x 𝒫
7 elpwi x 𝒫 x
8 ss0 x x =
9 6 7 8 3syl x 𝒫 Fin x =
10 9 inteqd x 𝒫 Fin x =
11 int0 = V
12 10 11 eqtrdi x 𝒫 Fin x = V
13 5 12 sylan9eqr x 𝒫 Fin y = x y = V
14 13 rexlimiva x 𝒫 Fin y = x y = V
15 vex y V
16 14 15 eqeltrrdi x 𝒫 Fin y = x V V
17 4 16 mto ¬ x 𝒫 Fin y = x
18 17 abf y | x 𝒫 Fin y = x =
19 3 18 eqtri fi =