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	$$⊢\phi \to \underset{\dot{}}{\sim }\mathrm{Er}V$$
	ercpbl.v	$$⊢\phi \to V\in W$$
	ercpbl.f	$$⊢F=\left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right)$$
Assertion	divsfval	$$⊢\phi \to F\left(A\right)=\left[A\right]\underset{\dot{}}{\sim }$$

Proof

Step	Hyp	Ref	Expression
1		ercpbl.r	$$⊢\phi \to \underset{\dot{}}{\sim }\mathrm{Er}V$$
2		ercpbl.v	$$⊢\phi \to V\in W$$
3		ercpbl.f	$$⊢F=\left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right)$$
4	1	ecss	$$⊢\phi \to \left[A\right]\underset{\dot{}}{\sim }\subseteq V$$
5	2 4	ssexd	$$⊢\phi \to \left[A\right]\underset{\dot{}}{\sim }\in \mathrm{V}$$
6		eceq1	$$⊢x=A\to \left[x\right]\underset{\dot{}}{\sim }=\left[A\right]\underset{\dot{}}{\sim }$$
7	6 3	fvmptg	$$⊢\left(A\in V\wedge \left[A\right]\underset{\dot{}}{\sim }\in \mathrm{V}\right)\to F\left(A\right)=\left[A\right]\underset{\dot{}}{\sim }$$
8	5 7	sylan2	$$⊢\left(A\in V\wedge \phi \right)\to F\left(A\right)=\left[A\right]\underset{\dot{}}{\sim }$$
9	8	expcom	$$⊢\phi \to \left(A\in V\to F\left(A\right)=\left[A\right]\underset{\dot{}}{\sim }\right)$$
10	3	dmeqi	$$⊢\mathrm{dom}F=\mathrm{dom}\left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right)$$
11	1	ecss	$$⊢\phi \to \left[x\right]\underset{\dot{}}{\sim }\subseteq V$$
12	2 11	ssexd	$$⊢\phi \to \left[x\right]\underset{\dot{}}{\sim }\in \mathrm{V}$$
13	12	ralrimivw	$$⊢\phi \to \forall x\in V\left[x\right]\underset{\dot{}}{\sim }\in \mathrm{V}$$
14		dmmptg	$$⊢\forall x\in V\left[x\right]\underset{\dot{}}{\sim }\in \mathrm{V}\to \mathrm{dom}\left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right)=V$$
15	13 14	syl	$$⊢\phi \to \mathrm{dom}\left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right)=V$$
16	10 15	eqtrid	$$⊢\phi \to \mathrm{dom}F=V$$
17	16	eleq2d	$$⊢\phi \to \left(A\in \mathrm{dom}F\leftrightarrow A\in V\right)$$
18	17	notbid	$$⊢\phi \to \left(\neg A\in \mathrm{dom}F\leftrightarrow \neg A\in V\right)$$
19		ndmfv	$$⊢\neg A\in \mathrm{dom}F\to F\left(A\right)=\varnothing$$
20	18 19	syl6bir	$$⊢\phi \to \left(\neg A\in V\to F\left(A\right)=\varnothing \right)$$
21		ecdmn0	$$⊢A\in \mathrm{dom}\underset{\dot{}}{\sim }\leftrightarrow \left[A\right]\underset{\dot{}}{\sim }\ne \varnothing$$
22		erdm	$$⊢\underset{\dot{}}{\sim }\mathrm{Er}V\to \mathrm{dom}\underset{\dot{}}{\sim }=V$$
23	1 22	syl	$$⊢\phi \to \mathrm{dom}\underset{\dot{}}{\sim }=V$$
24	23	eleq2d	$$⊢\phi \to \left(A\in \mathrm{dom}\underset{\dot{}}{\sim }\leftrightarrow A\in V\right)$$
25	24	biimpd	$$⊢\phi \to \left(A\in \mathrm{dom}\underset{\dot{}}{\sim }\to A\in V\right)$$
26	21 25	syl5bir	$$⊢\phi \to \left(\left[A\right]\underset{\dot{}}{\sim }\ne \varnothing \to A\in V\right)$$
27	26	necon1bd	$$⊢\phi \to \left(\neg A\in V\to \left[A\right]\underset{\dot{}}{\sim }=\varnothing \right)$$
28	20 27	jcad	$$⊢\phi \to \left(\neg A\in V\to \left(F\left(A\right)=\varnothing \wedge \left[A\right]\underset{\dot{}}{\sim }=\varnothing \right)\right)$$
29		eqtr3	$$⊢\left(F\left(A\right)=\varnothing \wedge \left[A\right]\underset{\dot{}}{\sim }=\varnothing \right)\to F\left(A\right)=\left[A\right]\underset{\dot{}}{\sim }$$
30	28 29	syl6	$$⊢\phi \to \left(\neg A\in V\to F\left(A\right)=\left[A\right]\underset{\dot{}}{\sim }\right)$$
31	9 30	pm2.61d	$$⊢\phi \to F\left(A\right)=\left[A\right]\underset{\dot{}}{\sim }$$