Theorem fvmptrab

Description: Value of a function mapping a set to a class abstraction restricting a class depending on the argument of the function. More general version of fvmptrabfv , but relying on the fact that out-of-domain arguments evaluate to the empty set, which relies on set.mm's particular encoding. (Contributed by AV, 14-Feb-2022)

	Ref	Expression
Hypotheses	fvmptrab.f	|- F = ( x e. V |-> { y e. M | ph } )
	fvmptrab.r	|- ( x = X -> ( ph <-> ps ) )
	fvmptrab.s	|- ( x = X -> M = N )
	fvmptrab.v	|- ( X e. V -> N e. _V )
	fvmptrab.n	|- ( X e/ V -> N = (/) )
Assertion	fvmptrab	|- ( F ` X ) = { y e. N | ps }

Proof

Step	Hyp	Ref	Expression
1		fvmptrab.f	|- F = ( x e. V |-> { y e. M | ph } )
2		fvmptrab.r	|- ( x = X -> ( ph <-> ps ) )
3		fvmptrab.s	|- ( x = X -> M = N )
4		fvmptrab.v	|- ( X e. V -> N e. _V )
5		fvmptrab.n	|- ( X e/ V -> N = (/) )
6	1	a1i	|- ( X e. V -> F = ( x e. V |-> { y e. M | ph } ) )
7	3 2	rabeqbidv	|- ( x = X -> { y e. M | ph } = { y e. N | ps } )
8	7	adantl	|- ( ( X e. V /\ x = X ) -> { y e. M | ph } = { y e. N | ps } )
9		id	|- ( X e. V -> X e. V )
10		eqid	|- { y e. N | ps } = { y e. N | ps }
11	10 4	rabexd	|- ( X e. V -> { y e. N | ps } e. _V )
12	6 8 9 11	fvmptd	|- ( X e. V -> ( F ` X ) = { y e. N | ps } )
13	1	fvmptndm	|- ( -. X e. V -> ( F ` X ) = (/) )
14		df-nel	|- ( X e/ V <-> -. X e. V )
15		rabeq	|- ( N = (/) -> { y e. N | ps } = { y e. (/) | ps } )
16		rab0	|- { y e. (/) | ps } = (/)
17	15 16	eqtr2di	|- ( N = (/) -> (/) = { y e. N | ps } )
18	5 17	syl	|- ( X e/ V -> (/) = { y e. N | ps } )
19	14 18	sylbir	|- ( -. X e. V -> (/) = { y e. N | ps } )
20	13 19	eqtrd	|- ( -. X e. V -> ( F ` X ) = { y e. N | ps } )
21	12 20	pm2.61i	|- ( F ` X ) = { y e. N | ps }