Metamath Proof Explorer

Theorem fsetprcnex

Description: The class of all functions from a nonempty set A into a proper class B is not a set. If one of the preconditions is not fufilled, then { f | f : A --> B } is a set, see fsetdmprc0 for A e/V , fset0 for A = (/) , and fsetex for B e. V , see also fsetexb . (Contributed by AV, 14-Sep-2024) (Proof shortened by BJ, 15-Sep-2024)

Ref Expression
Assertion fsetprcnex ⊢ A ∈ V ∧ A ≠ ∅ ∧ B ∉ V → f | f : A ⟶ B ∉ V

Proof

Step Hyp Ref Expression
1 n0 ⊢ A ≠ ∅ ↔ ∃ a a ∈ A
2 feq1 ⊢ f = m → f : A ⟶ B ↔ m : A ⟶ B
3 2 cbvabv ⊢ f | f : A ⟶ B = m | m : A ⟶ B
4 fveq1 ⊢ g = n → g ⁡ a = n ⁡ a
5 4 cbvmptv ⊢ g ∈ f | f : A ⟶ B ⟼ g ⁡ a = n ∈ f | f : A ⟶ B ⟼ n ⁡ a
6 3 5 fsetfocdm ⊢ A ∈ V ∧ a ∈ A → g ∈ f | f : A ⟶ B ⟼ g ⁡ a : f | f : A ⟶ B ⟶ onto B
7 fornex ⊢ f | f : A ⟶ B ∈ V → g ∈ f | f : A ⟶ B ⟼ g ⁡ a : f | f : A ⟶ B ⟶ onto B → B ∈ V
8 6 7 syl5com ⊢ A ∈ V ∧ a ∈ A → f | f : A ⟶ B ∈ V → B ∈ V
9 8 nelcon3d ⊢ A ∈ V ∧ a ∈ A → B ∉ V → f | f : A ⟶ B ∉ V
10 9 expcom ⊢ a ∈ A → A ∈ V → B ∉ V → f | f : A ⟶ B ∉ V
11 10 exlimiv ⊢ ∃ a a ∈ A → A ∈ V → B ∉ V → f | f : A ⟶ B ∉ V
12 1 11 sylbi ⊢ A ≠ ∅ → A ∈ V → B ∉ V → f | f : A ⟶ B ∉ V
13 12 impcom ⊢ A ∈ V ∧ A ≠ ∅ → B ∉ V → f | f : A ⟶ B ∉ V
14 13 imp ⊢ A ∈ V ∧ A ≠ ∅ ∧ B ∉ V → f | f : A ⟶ B ∉ V