Theorem fi0 7691

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

Assertion

Ref	Expression
fi0	|- ( fi ` (/) ) = (/)

Proof of Theorem fi0

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		0ex 4443	. . 3 |- (/) e. _V
2		fival 7683	. . 3 |- ( (/) e. _V -> ( fi ` (/) ) = { y | E. x e. ( ~P (/) i^i Fin ) y = |^| x } )
3	1, 2	ax-mp 5	. 2 |- ( fi ` (/) ) = { y | E. x e. ( ~P (/) i^i Fin ) y = |^| x }
4		vprc 4451	. . . 4 |- -. _V e. _V
5		id 22	. . . . . . 7 |- ( y = |^| x -> y = |^| x )
6		inss1 3591	. . . . . . . . . . 11 |- ( ~P (/) i^i Fin ) C_ ~P (/)
7	6	sseli 3373	. . . . . . . . . 10 |- ( x e. ( ~P (/) i^i Fin ) -> x e. ~P (/) )
8		elpwi 3890	. . . . . . . . . 10 |- ( x e. ~P (/) -> x C_ (/) )
9		ss0 3689	. . . . . . . . . 10 |- ( x C_ (/) -> x = (/) )
10	7, 8, 9	3syl 20	. . . . . . . . 9 |- ( x e. ( ~P (/) i^i Fin ) -> x = (/) )
11	10	inteqd 4154	. . . . . . . 8 |- ( x e. ( ~P (/) i^i Fin ) -> |^| x = |^| (/) )
12		int0 4163	. . . . . . . 8 |- |^| (/) = _V
13	11, 12	syl6eq 2491	. . . . . . 7 |- ( x e. ( ~P (/) i^i Fin ) -> |^| x = _V )
14	5, 13	sylan9eqr 2497	. . . . . 6 |- ( ( x e. ( ~P (/) i^i Fin ) /\ y = |^| x ) -> y = _V )
15	14	rexlimiva 2857	. . . . 5 |- ( E. x e. ( ~P (/) i^i Fin ) y = |^| x -> y = _V )
16		vex 2996	. . . . 5 |- y e. _V
17	15, 16	syl6eqelr 2532	. . . 4 |- ( E. x e. ( ~P (/) i^i Fin ) y = |^| x -> _V e. _V )
18	4, 17	mto 176	. . 3 |- -. E. x e. ( ~P (/) i^i Fin ) y = |^| x
19	18	abf 3692	. 2 |- { y | E. x e. ( ~P (/) i^i Fin ) y = |^| x } = (/)
20	3, 19	eqtri 2463	1 |- ( fi ` (/) ) = (/)

Syntax hints:   = wceq 1369   e. wcel 1756   {cab 2429   E.wrex 2737   _Vcvv 2993   i^i cin 3348   C_ wss 3349   (/)c0 3658   ~Pcpw 3881   |^|cint 4149   ` cfv 5439   Fincfn 7331   ficfi 7681

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552  ax-un 6393

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-sbc 3208  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-op 3905  df-uni 4113  df-int 4150  df-br 4314  df-opab 4372  df-mpt 4373  df-id 4657  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-iota 5402  df-fun 5441  df-fv 5447  df-fi 7682

This theorem is referenced by:  fieq0  7692  firest  14392  restbas  18784