Metamath Proof Explorer

Theorem mapprc

Description: When A is a proper class, the class of all functions mapping A to B is empty. Exercise 4.41 of Mendelson p. 255. (Contributed by NM, 8-Dec-2003)

Ref Expression
Assertion mapprc ⊢ ¬ A ∈ V → f | f : A ⟶ B = ∅

Proof

Step Hyp Ref Expression
1 abn0 ⊢ f | f : A ⟶ B ≠ ∅ ↔ ∃ f f : A ⟶ B
2 fdm ⊢ f : A ⟶ B → dom ⁡ f = A
3 vex ⊢ f ∈ V
4 3 dmex ⊢ dom ⁡ f ∈ V
5 2 4 eqeltrrdi ⊢ f : A ⟶ B → A ∈ V
6 5 exlimiv ⊢ ∃ f f : A ⟶ B → A ∈ V
7 1 6 sylbi ⊢ f | f : A ⟶ B ≠ ∅ → A ∈ V
8 7 necon1bi ⊢ ¬ A ∈ V → f | f : A ⟶ B = ∅