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 ( ( 𝐵𝑉𝐴𝐵 ) → ( 𝐴m 𝐶 ) ⊆ ( 𝐵m 𝐶 ) )

Proof

Step Hyp Ref Expression
1 elmapi ( 𝑓 ∈ ( 𝐴m 𝐶 ) → 𝑓 : 𝐶𝐴 )
2 1 adantl ( ( ( 𝐵𝑉𝐴𝐵 ) ∧ 𝑓 ∈ ( 𝐴m 𝐶 ) ) → 𝑓 : 𝐶𝐴 )
3 simplr ( ( ( 𝐵𝑉𝐴𝐵 ) ∧ 𝑓 ∈ ( 𝐴m 𝐶 ) ) → 𝐴𝐵 )
4 2 3 fssd ( ( ( 𝐵𝑉𝐴𝐵 ) ∧ 𝑓 ∈ ( 𝐴m 𝐶 ) ) → 𝑓 : 𝐶𝐵 )
5 simpll ( ( ( 𝐵𝑉𝐴𝐵 ) ∧ 𝑓 ∈ ( 𝐴m 𝐶 ) ) → 𝐵𝑉 )
6 elmapex ( 𝑓 ∈ ( 𝐴m 𝐶 ) → ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) )
7 6 simprd ( 𝑓 ∈ ( 𝐴m 𝐶 ) → 𝐶 ∈ V )
8 7 adantl ( ( ( 𝐵𝑉𝐴𝐵 ) ∧ 𝑓 ∈ ( 𝐴m 𝐶 ) ) → 𝐶 ∈ V )
9 5 8 elmapd ( ( ( 𝐵𝑉𝐴𝐵 ) ∧ 𝑓 ∈ ( 𝐴m 𝐶 ) ) → ( 𝑓 ∈ ( 𝐵m 𝐶 ) ↔ 𝑓 : 𝐶𝐵 ) )
10 4 9 mpbird ( ( ( 𝐵𝑉𝐴𝐵 ) ∧ 𝑓 ∈ ( 𝐴m 𝐶 ) ) → 𝑓 ∈ ( 𝐵m 𝐶 ) )
11 10 ex ( ( 𝐵𝑉𝐴𝐵 ) → ( 𝑓 ∈ ( 𝐴m 𝐶 ) → 𝑓 ∈ ( 𝐵m 𝐶 ) ) )
12 11 ssrdv ( ( 𝐵𝑉𝐴𝐵 ) → ( 𝐴m 𝐶 ) ⊆ ( 𝐵m 𝐶 ) )