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	⊢ 𝑃 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) }
Assertion	0nelsetpreimafv	⊢ ( 𝐹 Fn 𝐴 → ∅ ∉ 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		setpreimafvex.p	⊢ 𝑃 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) }
2		preimafvsnel	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) )
3		n0i	⊢ ( 𝑥 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) → ¬ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) = ∅ )
4	2 3	syl	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ¬ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) = ∅ )
5	4	ralrimiva	⊢ ( 𝐹 Fn 𝐴 → ∀ 𝑥 ∈ 𝐴 ¬ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) = ∅ )
6		ralnex	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ ∅ = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ↔ ¬ ∃ 𝑥 ∈ 𝐴 ∅ = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) )
7		eqcom	⊢ ( ∅ = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ↔ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) = ∅ )
8	7	notbii	⊢ ( ¬ ∅ = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ↔ ¬ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) = ∅ )
9	8	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ ∅ = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ↔ ∀ 𝑥 ∈ 𝐴 ¬ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) = ∅ )
10	6 9	bitr3i	⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ∅ = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ↔ ∀ 𝑥 ∈ 𝐴 ¬ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) = ∅ )
11	5 10	sylibr	⊢ ( 𝐹 Fn 𝐴 → ¬ ∃ 𝑥 ∈ 𝐴 ∅ = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) )
12		0ex	⊢ ∅ ∈ V
13	1	elsetpreimafvb	⊢ ( ∅ ∈ V → ( ∅ ∈ 𝑃 ↔ ∃ 𝑥 ∈ 𝐴 ∅ = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) )
14	12 13	ax-mp	⊢ ( ∅ ∈ 𝑃 ↔ ∃ 𝑥 ∈ 𝐴 ∅ = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) )
15	11 14	sylnibr	⊢ ( 𝐹 Fn 𝐴 → ¬ ∅ ∈ 𝑃 )
16		df-nel	⊢ ( ∅ ∉ 𝑃 ↔ ¬ ∅ ∈ 𝑃 )
17	15 16	sylibr	⊢ ( 𝐹 Fn 𝐴 → ∅ ∉ 𝑃 )