Theorem elmapssres

Description: A restricted mapping is a mapping. (Contributed by Stefan O'Rear, 9-Oct-2014) (Revised by Mario Carneiro, 5-May-2015)

	Ref	Expression
Assertion	elmapssres	⊢ ( ( 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) ∧ 𝐷 ⊆ 𝐶 ) → ( 𝐴 ↾ 𝐷 ) ∈ ( 𝐵 ↑m 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		elmapi	⊢ ( 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) → 𝐴 : 𝐶 ⟶ 𝐵 )
2		fssres	⊢ ( ( 𝐴 : 𝐶 ⟶ 𝐵 ∧ 𝐷 ⊆ 𝐶 ) → ( 𝐴 ↾ 𝐷 ) : 𝐷 ⟶ 𝐵 )
3	1 2	sylan	⊢ ( ( 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) ∧ 𝐷 ⊆ 𝐶 ) → ( 𝐴 ↾ 𝐷 ) : 𝐷 ⟶ 𝐵 )
4		elmapex	⊢ ( 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) → ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) )
5	4	simpld	⊢ ( 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) → 𝐵 ∈ V )
6	5	adantr	⊢ ( ( 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) ∧ 𝐷 ⊆ 𝐶 ) → 𝐵 ∈ V )
7	4	simprd	⊢ ( 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) → 𝐶 ∈ V )
8		ssexg	⊢ ( ( 𝐷 ⊆ 𝐶 ∧ 𝐶 ∈ V ) → 𝐷 ∈ V )
9	8	ancoms	⊢ ( ( 𝐶 ∈ V ∧ 𝐷 ⊆ 𝐶 ) → 𝐷 ∈ V )
10	7 9	sylan	⊢ ( ( 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) ∧ 𝐷 ⊆ 𝐶 ) → 𝐷 ∈ V )
11	6 10	elmapd	⊢ ( ( 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) ∧ 𝐷 ⊆ 𝐶 ) → ( ( 𝐴 ↾ 𝐷 ) ∈ ( 𝐵 ↑m 𝐷 ) ↔ ( 𝐴 ↾ 𝐷 ) : 𝐷 ⟶ 𝐵 ) )
12	3 11	mpbird	⊢ ( ( 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) ∧ 𝐷 ⊆ 𝐶 ) → ( 𝐴 ↾ 𝐷 ) ∈ ( 𝐵 ↑m 𝐷 ) )