Theorem divsfval

Description: Value of the function in qusval . (Contributed by Mario Carneiro, 24-Feb-2015) (Revised by Mario Carneiro, 12-Aug-2015) (Revised by AV, 12-Jul-2024)

	Ref	Expression
Hypotheses	ercpbl.r	|- ( ph -> .~ Er V )
	ercpbl.v	|- ( ph -> V e. W )
	ercpbl.f	|- F = ( x e. V |-> [ x ] .~ )
Assertion	divsfval	|- ( ph -> ( F ` A ) = [ A ] .~ )

Proof

Step	Hyp	Ref	Expression
1		ercpbl.r	|- ( ph -> .~ Er V )
2		ercpbl.v	|- ( ph -> V e. W )
3		ercpbl.f	|- F = ( x e. V |-> [ x ] .~ )
4	1	ecss	|- ( ph -> [ A ] .~ C_ V )
5	2 4	ssexd	|- ( ph -> [ A ] .~ e. _V )
6		eceq1	|- ( x = A -> [ x ] .~ = [ A ] .~ )
7	6 3	fvmptg	|- ( ( A e. V /\ [ A ] .~ e. _V ) -> ( F ` A ) = [ A ] .~ )
8	5 7	sylan2	|- ( ( A e. V /\ ph ) -> ( F ` A ) = [ A ] .~ )
9	8	expcom	|- ( ph -> ( A e. V -> ( F ` A ) = [ A ] .~ ) )
10	3	dmeqi	|- dom F = dom ( x e. V |-> [ x ] .~ )
11	1	ecss	|- ( ph -> [ x ] .~ C_ V )
12	2 11	ssexd	|- ( ph -> [ x ] .~ e. _V )
13	12	ralrimivw	|- ( ph -> A. x e. V [ x ] .~ e. _V )
14		dmmptg	|- ( A. x e. V [ x ] .~ e. _V -> dom ( x e. V |-> [ x ] .~ ) = V )
15	13 14	syl	|- ( ph -> dom ( x e. V |-> [ x ] .~ ) = V )
16	10 15	eqtrid	|- ( ph -> dom F = V )
17	16	eleq2d	|- ( ph -> ( A e. dom F <-> A e. V ) )
18	17	notbid	|- ( ph -> ( -. A e. dom F <-> -. A e. V ) )
19		ndmfv	|- ( -. A e. dom F -> ( F ` A ) = (/) )
20	18 19	syl6bir	|- ( ph -> ( -. A e. V -> ( F ` A ) = (/) ) )
21		ecdmn0	|- ( A e. dom .~ <-> [ A ] .~ =/= (/) )
22		erdm	|- ( .~ Er V -> dom .~ = V )
23	1 22	syl	|- ( ph -> dom .~ = V )
24	23	eleq2d	|- ( ph -> ( A e. dom .~ <-> A e. V ) )
25	24	biimpd	|- ( ph -> ( A e. dom .~ -> A e. V ) )
26	21 25	syl5bir	|- ( ph -> ( [ A ] .~ =/= (/) -> A e. V ) )
27	26	necon1bd	|- ( ph -> ( -. A e. V -> [ A ] .~ = (/) ) )
28	20 27	jcad	|- ( ph -> ( -. A e. V -> ( ( F ` A ) = (/) /\ [ A ] .~ = (/) ) ) )
29		eqtr3	|- ( ( ( F ` A ) = (/) /\ [ A ] .~ = (/) ) -> ( F ` A ) = [ A ] .~ )
30	28 29	syl6	|- ( ph -> ( -. A e. V -> ( F ` A ) = [ A ] .~ ) )
31	9 30	pm2.61d	|- ( ph -> ( F ` A ) = [ A ] .~ )