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

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 𝐶 ) )