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

Metamath Proof Explorer

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 ⊢ ( 𝐹 ‘ 𝐷 ) ⊆ 𝐶