Theorem mapex

Description: The class of all functions mapping one set to another is a set. Remark after Definition 10.24 of Kunen p. 31. (Contributed by Raph Levien, 4-Dec-2003)

	Ref	Expression
Assertion	mapex	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		fssxp	⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → 𝑓 ⊆ ( 𝐴 × 𝐵 ) )
2	1	ss2abi	⊢ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ⊆ { 𝑓 ∣ 𝑓 ⊆ ( 𝐴 × 𝐵 ) }
3		df-pw	⊢ 𝒫 ( 𝐴 × 𝐵 ) = { 𝑓 ∣ 𝑓 ⊆ ( 𝐴 × 𝐵 ) }
4	2 3	sseqtrri	⊢ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ⊆ 𝒫 ( 𝐴 × 𝐵 )
5		xpexg	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 × 𝐵 ) ∈ V )
6	5	pwexd	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → 𝒫 ( 𝐴 × 𝐵 ) ∈ V )
7		ssexg	⊢ ( ( { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ⊆ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝒫 ( 𝐴 × 𝐵 ) ∈ V ) → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V )
8	4 6 7	sylancr	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V )