Metamath Proof Explorer

Theorem mapss

Description: Subset inheritance for set exponentiation. Theorem 99 of Suppes p. 89. (Contributed by NM, 10-Dec-2003) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Assertion mapss ⊢ B ∈ V ∧ A ⊆ B → A C ⊆ B C

Proof

Step Hyp Ref Expression
1 elmapi ⊢ f ∈ A C → f : C ⟶ A
2 1 adantl ⊢ B ∈ V ∧ A ⊆ B ∧ f ∈ A C → f : C ⟶ A
3 simplr ⊢ B ∈ V ∧ A ⊆ B ∧ f ∈ A C → A ⊆ B
4 2 3 fssd ⊢ B ∈ V ∧ A ⊆ B ∧ f ∈ A C → f : C ⟶ B
5 simpll ⊢ B ∈ V ∧ A ⊆ B ∧ f ∈ A C → B ∈ V
6 elmapex ⊢ f ∈ A C → A ∈ V ∧ C ∈ V
7 6 simprd ⊢ f ∈ A C → C ∈ V
8 7 adantl ⊢ B ∈ V ∧ A ⊆ B ∧ f ∈ A C → C ∈ V
9 5 8 elmapd ⊢ B ∈ V ∧ A ⊆ B ∧ f ∈ A C → f ∈ B C ↔ f : C ⟶ B
10 4 9 mpbird ⊢ B ∈ V ∧ A ⊆ B ∧ f ∈ A C → f ∈ B C
11 10 ex ⊢ B ∈ V ∧ A ⊆ B → f ∈ A C → f ∈ B C
12 11 ssrdv ⊢ B ∈ V ∧ A ⊆ B → A C ⊆ B C