Theorem mapfoss

Description: The value of the set exponentiation ( B ^m A ) is a superset of the set of all functions from A onto B . (Contributed by AV, 7-Aug-2024)

	Ref	Expression
Assertion	mapfoss	⊢ { 𝑓 ∣ 𝑓 : 𝐴 –onto→ 𝐵 } ⊆ ( 𝐵 ↑m 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑚 ∈ V
2		foeq1	⊢ ( 𝑓 = 𝑚 → ( 𝑓 : 𝐴 –onto→ 𝐵 ↔ 𝑚 : 𝐴 –onto→ 𝐵 ) )
3	1 2	elab	⊢ ( 𝑚 ∈ { 𝑓 ∣ 𝑓 : 𝐴 –onto→ 𝐵 } ↔ 𝑚 : 𝐴 –onto→ 𝐵 )
4		fof	⊢ ( 𝑚 : 𝐴 –onto→ 𝐵 → 𝑚 : 𝐴 ⟶ 𝐵 )
5		forn	⊢ ( 𝑚 : 𝐴 –onto→ 𝐵 → ran 𝑚 = 𝐵 )
6	1	rnex	⊢ ran 𝑚 ∈ V
7	5 6	eqeltrrdi	⊢ ( 𝑚 : 𝐴 –onto→ 𝐵 → 𝐵 ∈ V )
8		dmfex	⊢ ( ( 𝑚 ∈ V ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) → 𝐴 ∈ V )
9	1 4 8	sylancr	⊢ ( 𝑚 : 𝐴 –onto→ 𝐵 → 𝐴 ∈ V )
10	7 9	elmapd	⊢ ( 𝑚 : 𝐴 –onto→ 𝐵 → ( 𝑚 ∈ ( 𝐵 ↑m 𝐴 ) ↔ 𝑚 : 𝐴 ⟶ 𝐵 ) )
11	4 10	mpbird	⊢ ( 𝑚 : 𝐴 –onto→ 𝐵 → 𝑚 ∈ ( 𝐵 ↑m 𝐴 ) )
12	3 11	sylbi	⊢ ( 𝑚 ∈ { 𝑓 ∣ 𝑓 : 𝐴 –onto→ 𝐵 } → 𝑚 ∈ ( 𝐵 ↑m 𝐴 ) )
13	12	ssriv	⊢ { 𝑓 ∣ 𝑓 : 𝐴 –onto→ 𝐵 } ⊆ ( 𝐵 ↑m 𝐴 )