Theorem fvmptss

Description: If all the values of the mapping are subsets of a class C , then so is any evaluation of the mapping, even if D is not in the base set A . (Contributed by Mario Carneiro, 13-Feb-2015)

	Ref	Expression
Hypothesis	mptrcl.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
Assertion	fvmptss	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ( 𝐹 ‘ 𝐷 ) ⊆ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		mptrcl.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2	1	dmmptss	⊢ dom 𝐹 ⊆ 𝐴
3	2	sseli	⊢ ( 𝐷 ∈ dom 𝐹 → 𝐷 ∈ 𝐴 )
4		fveq2	⊢ ( 𝑦 = 𝐷 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐷 ) )
5	4	sseq1d	⊢ ( 𝑦 = 𝐷 → ( ( 𝐹 ‘ 𝑦 ) ⊆ 𝐶 ↔ ( 𝐹 ‘ 𝐷 ) ⊆ 𝐶 ) )
6	5	imbi2d	⊢ ( 𝑦 = 𝐷 → ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ( 𝐹 ‘ 𝑦 ) ⊆ 𝐶 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ( 𝐹 ‘ 𝐷 ) ⊆ 𝐶 ) ) )
7		nfcv	⊢ Ⅎ 𝑥 𝑦
8		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶
9		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
10	1 9	nfcxfr	⊢ Ⅎ 𝑥 𝐹
11	10 7	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑦 )
12		nfcv	⊢ Ⅎ 𝑥 𝐶
13	11 12	nfss	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ 𝐶
14	8 13	nfim	⊢ Ⅎ 𝑥 ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ( 𝐹 ‘ 𝑦 ) ⊆ 𝐶 )
15		fveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
16	15	sseq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) ⊆ 𝐶 ↔ ( 𝐹 ‘ 𝑦 ) ⊆ 𝐶 ) )
17	16	imbi2d	⊢ ( 𝑥 = 𝑦 → ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ( 𝐹 ‘ 𝑥 ) ⊆ 𝐶 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ( 𝐹 ‘ 𝑦 ) ⊆ 𝐶 ) ) )
18	1	dmmpt	⊢ dom 𝐹 = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V }
19	18	reqabi	⊢ ( 𝑥 ∈ dom 𝐹 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ V ) )
20	1	fvmpt2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ V ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
21		eqimss	⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝐵 → ( 𝐹 ‘ 𝑥 ) ⊆ 𝐵 )
22	20 21	syl	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ V ) → ( 𝐹 ‘ 𝑥 ) ⊆ 𝐵 )
23	19 22	sylbi	⊢ ( 𝑥 ∈ dom 𝐹 → ( 𝐹 ‘ 𝑥 ) ⊆ 𝐵 )
24		ndmfv	⊢ ( ¬ 𝑥 ∈ dom 𝐹 → ( 𝐹 ‘ 𝑥 ) = ∅ )
25		0ss	⊢ ∅ ⊆ 𝐵
26	24 25	eqsstrdi	⊢ ( ¬ 𝑥 ∈ dom 𝐹 → ( 𝐹 ‘ 𝑥 ) ⊆ 𝐵 )
27	23 26	pm2.61i	⊢ ( 𝐹 ‘ 𝑥 ) ⊆ 𝐵
28		rsp	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ( 𝑥 ∈ 𝐴 → 𝐵 ⊆ 𝐶 ) )
29	28	impcom	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ) → 𝐵 ⊆ 𝐶 )
30	27 29	sstrid	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ) → ( 𝐹 ‘ 𝑥 ) ⊆ 𝐶 )
31	30	ex	⊢ ( 𝑥 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ( 𝐹 ‘ 𝑥 ) ⊆ 𝐶 ) )
32	7 14 17 31	vtoclgaf	⊢ ( 𝑦 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ( 𝐹 ‘ 𝑦 ) ⊆ 𝐶 ) )
33	6 32	vtoclga	⊢ ( 𝐷 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ( 𝐹 ‘ 𝐷 ) ⊆ 𝐶 ) )
34	33	impcom	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ∧ 𝐷 ∈ 𝐴 ) → ( 𝐹 ‘ 𝐷 ) ⊆ 𝐶 )
35	3 34	sylan2	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ∧ 𝐷 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝐷 ) ⊆ 𝐶 )
36		ndmfv	⊢ ( ¬ 𝐷 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐷 ) = ∅ )
37	36	adantl	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ∧ ¬ 𝐷 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝐷 ) = ∅ )
38		0ss	⊢ ∅ ⊆ 𝐶
39	37 38	eqsstrdi	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ∧ ¬ 𝐷 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝐷 ) ⊆ 𝐶 )
40	35 39	pm2.61dan	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ( 𝐹 ‘ 𝐷 ) ⊆ 𝐶 )