This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ f | f : A ⟶ onto B ⊆ B A

Proof

Step Hyp Ref Expression
1 vex ⊢ m ∈ V
2 foeq1 ⊢ f = m → f : A ⟶ onto B ↔ m : A ⟶ onto B
3 1 2 elab ⊢ m ∈ f | f : A ⟶ onto B ↔ m : A ⟶ onto B
4 fof ⊢ m : A ⟶ onto B → m : A ⟶ B
5 forn ⊢ m : A ⟶ onto B → ran ⁡ m = B
6 1 rnex ⊢ ran ⁡ m ∈ V
7 5 6 eqeltrrdi ⊢ m : A ⟶ onto B → B ∈ V
8 dmfex ⊢ m ∈ V ∧ m : A ⟶ B → A ∈ V
9 1 4 8 sylancr ⊢ m : A ⟶ onto B → A ∈ V
10 7 9 elmapd ⊢ m : A ⟶ onto B → m ∈ B A ↔ m : A ⟶ B
11 4 10 mpbird ⊢ m : A ⟶ onto B → m ∈ B A
12 3 11 sylbi ⊢ m ∈ f | f : A ⟶ onto B → m ∈ B A
13 12 ssriv ⊢ f | f : A ⟶ onto B ⊆ B A