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

Metamath Proof Explorer

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