Metamath Proof Explorer

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 | ∃ x ∈ A z = F -1 F ⁡ x
Assertion 0nelsetpreimafv ⊢ F Fn A → ∅ ∉ P

Proof

Step Hyp Ref Expression
1 setpreimafvex.p ⊢ P = z | ∃ x ∈ A z = F -1 F ⁡ x
2 preimafvsnel ⊢ F Fn A ∧ x ∈ A → x ∈ F -1 F ⁡ x
3 n0i ⊢ x ∈ F -1 F ⁡ x → ¬ F -1 F ⁡ x = ∅
4 2 3 syl ⊢ F Fn A ∧ x ∈ A → ¬ F -1 F ⁡ x = ∅
5 4 ralrimiva ⊢ F Fn A → ∀ x ∈ A ¬ F -1 F ⁡ x = ∅
6 ralnex ⊢ ∀ x ∈ A ¬ ∅ = F -1 F ⁡ x ↔ ¬ ∃ x ∈ A ∅ = F -1 F ⁡ x
7 eqcom ⊢ ∅ = F -1 F ⁡ x ↔ F -1 F ⁡ x = ∅
8 7 notbii ⊢ ¬ ∅ = F -1 F ⁡ x ↔ ¬ F -1 F ⁡ x = ∅
9 8 ralbii ⊢ ∀ x ∈ A ¬ ∅ = F -1 F ⁡ x ↔ ∀ x ∈ A ¬ F -1 F ⁡ x = ∅
10 6 9 bitr3i ⊢ ¬ ∃ x ∈ A ∅ = F -1 F ⁡ x ↔ ∀ x ∈ A ¬ F -1 F ⁡ x = ∅
11 5 10 sylibr ⊢ F Fn A → ¬ ∃ x ∈ A ∅ = F -1 F ⁡ x
12 0ex ⊢ ∅ ∈ V
13 1 elsetpreimafvb ⊢ ∅ ∈ V → ∅ ∈ P ↔ ∃ x ∈ A ∅ = F -1 F ⁡ x
14 12 13 ax-mp ⊢ ∅ ∈ P ↔ ∃ x ∈ A ∅ = F -1 F ⁡ x
15 11 14 sylnibr ⊢ F Fn A → ¬ ∅ ∈ P
16 df-nel ⊢ ∅ ∉ P ↔ ¬ ∅ ∈ P
17 15 16 sylibr ⊢ F Fn A → ∅ ∉ P