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 ⊢ x = D → B = C
fvmptn.2 ⊢ F = x ∈ A ⟼ B
Assertion fvmptss2 ⊢ F ⁡ D ⊆ C

Proof

Step Hyp Ref Expression
1 fvmptn.1 ⊢ x = D → B = C
2 fvmptn.2 ⊢ F = x ∈ A ⟼ B
3 1 eleq1d ⊢ x = D → B ∈ V ↔ C ∈ V
4 2 dmmpt ⊢ dom ⁡ F = x ∈ A | B ∈ V
5 3 4 elrab2 ⊢ D ∈ dom ⁡ F ↔ D ∈ A ∧ C ∈ V
6 1 2 fvmptg ⊢ D ∈ A ∧ C ∈ V → F ⁡ D = C
7 eqimss ⊢ F ⁡ D = C → F ⁡ D ⊆ C
8 6 7 syl ⊢ D ∈ A ∧ C ∈ V → F ⁡ D ⊆ C
9 5 8 sylbi ⊢ D ∈ dom ⁡ F → F ⁡ D ⊆ C
10 ndmfv ⊢ ¬ D ∈ dom ⁡ F → F ⁡ D = ∅
11 0ss ⊢ ∅ ⊆ C
12 10 11 eqsstrdi ⊢ ¬ D ∈ dom ⁡ F → F ⁡ D ⊆ C
13 9 12 pm2.61i ⊢ F ⁡ D ⊆ C