Theorem 0nelsetpreimafv

Description: The empty set is not an element of the class P of all preimages of function values. (Contributed by AV, 6-Mar-2024)

	Ref	Expression
Hypothesis	setpreimafvex.p	|- P = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
Assertion	0nelsetpreimafv	|- ( F Fn A -> (/) e/ P )

Proof

Step	Hyp	Ref	Expression
1		setpreimafvex.p	|- P = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
2		preimafvsnel	|- ( ( F Fn A /\ x e. A ) -> x e. ( `' F " { ( F ` x ) } ) )
3		n0i	|- ( x e. ( `' F " { ( F ` x ) } ) -> -. ( `' F " { ( F ` x ) } ) = (/) )
4	2 3	syl	|- ( ( F Fn A /\ x e. A ) -> -. ( `' F " { ( F ` x ) } ) = (/) )
5	4	ralrimiva	|- ( F Fn A -> A. x e. A -. ( `' F " { ( F ` x ) } ) = (/) )
6		ralnex	|- ( A. x e. A -. (/) = ( `' F " { ( F ` x ) } ) <-> -. E. x e. A (/) = ( `' F " { ( F ` x ) } ) )
7		eqcom	|- ( (/) = ( `' F " { ( F ` x ) } ) <-> ( `' F " { ( F ` x ) } ) = (/) )
8	7	notbii	|- ( -. (/) = ( `' F " { ( F ` x ) } ) <-> -. ( `' F " { ( F ` x ) } ) = (/) )
9	8	ralbii	|- ( A. x e. A -. (/) = ( `' F " { ( F ` x ) } ) <-> A. x e. A -. ( `' F " { ( F ` x ) } ) = (/) )
10	6 9	bitr3i	|- ( -. E. x e. A (/) = ( `' F " { ( F ` x ) } ) <-> A. x e. A -. ( `' F " { ( F ` x ) } ) = (/) )
11	5 10	sylibr	|- ( F Fn A -> -. E. x e. A (/) = ( `' F " { ( F ` x ) } ) )
12		0ex	|- (/) e. _V
13	1	elsetpreimafvb	|- ( (/) e. _V -> ( (/) e. P <-> E. x e. A (/) = ( `' F " { ( F ` x ) } ) ) )
14	12 13	ax-mp	|- ( (/) e. P <-> E. x e. A (/) = ( `' F " { ( F ` x ) } ) )
15	11 14	sylnibr	|- ( F Fn A -> -. (/) e. P )
16		df-nel	|- ( (/) e/ P <-> -. (/) e. P )
17	15 16	sylibr	|- ( F Fn A -> (/) e/ P )