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	⊢ ( ¬ 𝐴 ∈ V → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } = ∅ )

Proof

Step	Hyp	Ref	Expression
1		abn0	⊢ ( { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ≠ ∅ ↔ ∃ 𝑓 𝑓 : 𝐴 ⟶ 𝐵 )
2		fdm	⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → dom 𝑓 = 𝐴 )
3		vex	⊢ 𝑓 ∈ V
4	3	dmex	⊢ dom 𝑓 ∈ V
5	2 4	eqeltrrdi	⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → 𝐴 ∈ V )
6	5	exlimiv	⊢ ( ∃ 𝑓 𝑓 : 𝐴 ⟶ 𝐵 → 𝐴 ∈ V )
7	1 6	sylbi	⊢ ( { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ≠ ∅ → 𝐴 ∈ V )
8	7	necon1bi	⊢ ( ¬ 𝐴 ∈ V → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } = ∅ )