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