Theorem fvmptss2

Description: A mapping always evaluates to a subset of the substituted expression in the mapping, even if this is a proper class, or we are out of the domain. (Contributed by Mario Carneiro, 13-Feb-2015)

	Ref	Expression
Hypotheses	fvmptn.1	⊢ ( 𝑥 = 𝐷 → 𝐵 = 𝐶 )
	fvmptn.2	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
Assertion	fvmptss2	⊢ ( 𝐹 ‘ 𝐷 ) ⊆ 𝐶

Proof

Step	Hyp	Ref	Expression
1		fvmptn.1	⊢ ( 𝑥 = 𝐷 → 𝐵 = 𝐶 )
2		fvmptn.2	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
3	1	eleq1d	⊢ ( 𝑥 = 𝐷 → ( 𝐵 ∈ V ↔ 𝐶 ∈ V ) )
4	2	dmmpt	⊢ dom 𝐹 = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V }
5	3 4	elrab2	⊢ ( 𝐷 ∈ dom 𝐹 ↔ ( 𝐷 ∈ 𝐴 ∧ 𝐶 ∈ V ) )
6	1 2	fvmptg	⊢ ( ( 𝐷 ∈ 𝐴 ∧ 𝐶 ∈ V ) → ( 𝐹 ‘ 𝐷 ) = 𝐶 )
7		eqimss	⊢ ( ( 𝐹 ‘ 𝐷 ) = 𝐶 → ( 𝐹 ‘ 𝐷 ) ⊆ 𝐶 )
8	6 7	syl	⊢ ( ( 𝐷 ∈ 𝐴 ∧ 𝐶 ∈ V ) → ( 𝐹 ‘ 𝐷 ) ⊆ 𝐶 )
9	5 8	sylbi	⊢ ( 𝐷 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐷 ) ⊆ 𝐶 )
10		ndmfv	⊢ ( ¬ 𝐷 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐷 ) = ∅ )
11		0ss	⊢ ∅ ⊆ 𝐶
12	10 11	eqsstrdi	⊢ ( ¬ 𝐷 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐷 ) ⊆ 𝐶 )
13	9 12	pm2.61i	⊢ ( 𝐹 ‘ 𝐷 ) ⊆ 𝐶