Theorem dffv2

Description: Alternate definition of function value df-fv that doesn't require dummy variables. (Contributed by NM, 4-Aug-2010)

	Ref	Expression
Assertion	dffv2	$$⊢F\left(A\right)=\bigcup \left(F\left[\left\{A\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		snidb	$$⊢A\in \mathrm{V}\leftrightarrow A\in \left\{A\right\}$$
2		fvres	$$⊢A\in \left\{A\right\}\to \left({F\upharpoonright }_{\left\{A\right\}}\right)\left(A\right)=F\left(A\right)$$
3	1 2	sylbi	$$⊢A\in \mathrm{V}\to \left({F\upharpoonright }_{\left\{A\right\}}\right)\left(A\right)=F\left(A\right)$$
4		fvprc	$$⊢\neg A\in \mathrm{V}\to \left({F\upharpoonright }_{\left\{A\right\}}\right)\left(A\right)=\varnothing$$
5		fvprc	$$⊢\neg A\in \mathrm{V}\to F\left(A\right)=\varnothing$$
6	4 5	eqtr4d	$$⊢\neg A\in \mathrm{V}\to \left({F\upharpoonright }_{\left\{A\right\}}\right)\left(A\right)=F\left(A\right)$$
7	3 6	pm2.61i	$$⊢\left({F\upharpoonright }_{\left\{A\right\}}\right)\left(A\right)=F\left(A\right)$$
8		funfv	$$⊢\mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to \left({F\upharpoonright }_{\left\{A\right\}}\right)\left(A\right)=\bigcup \left({F\upharpoonright }_{\left\{A\right\}}\right)\left[\left\{A\right\}\right]$$
9		resima	$$⊢\left({F\upharpoonright }_{\left\{A\right\}}\right)\left[\left\{A\right\}\right]=F\left[\left\{A\right\}\right]$$
10		dif0	$$⊢F\left[\left\{A\right\}\right]\setminus \varnothing =F\left[\left\{A\right\}\right]$$
11	9 10	eqtr4i	$$⊢\left({F\upharpoonright }_{\left\{A\right\}}\right)\left[\left\{A\right\}\right]=F\left[\left\{A\right\}\right]\setminus \varnothing$$
12		df-fun	$$⊢\mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\leftrightarrow \left(\mathrm{Rel}\left({F\upharpoonright }_{\left\{A\right\}}\right)\wedge \left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\subseteq \mathrm{I}\right)$$
13	12	simprbi	$$⊢\mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to \left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\subseteq \mathrm{I}$$
14		ssdif0	$$⊢\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\subseteq \mathrm{I}\leftrightarrow \left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}=\varnothing$$
15	13 14	sylib	$$⊢\mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to \left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}=\varnothing$$
16	15	unieqd	$$⊢\mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)=\bigcup \varnothing$$
17		uni0	$$⊢\bigcup \varnothing =\varnothing$$
18	16 17	eqtrdi	$$⊢\mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)=\varnothing$$
19	18	unieqd	$$⊢\mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)=\bigcup \varnothing$$
20	19 17	eqtrdi	$$⊢\mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)=\varnothing$$
21	20	difeq2d	$$⊢\mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to F\left[\left\{A\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)=F\left[\left\{A\right\}\right]\setminus \varnothing$$
22	11 21	eqtr4id	$$⊢\mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to \left({F\upharpoonright }_{\left\{A\right\}}\right)\left[\left\{A\right\}\right]=F\left[\left\{A\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)$$
23	22	unieqd	$$⊢\mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to \bigcup \left({F\upharpoonright }_{\left\{A\right\}}\right)\left[\left\{A\right\}\right]=\bigcup \left(F\left[\left\{A\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\right)$$
24	8 23	eqtrd	$$⊢\mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to \left({F\upharpoonright }_{\left\{A\right\}}\right)\left(A\right)=\bigcup \left(F\left[\left\{A\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\right)$$
25	7 24	syl5eqr	$$⊢\mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to F\left(A\right)=\bigcup \left(F\left[\left\{A\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\right)$$
26		nfunsn	$$⊢\neg \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to F\left(A\right)=\varnothing$$
27		relres	$$⊢\mathrm{Rel}\left({F\upharpoonright }_{\left\{A\right\}}\right)$$
28		dffun3	$$⊢\mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\leftrightarrow \left(\mathrm{Rel}\left({F\upharpoonright }_{\left\{A\right\}}\right)\wedge \forall x\exists y\forall z\left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\to z=y\right)\right)$$
29	27 28	mpbiran	$$⊢\mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\leftrightarrow \forall x\exists y\forall z\left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\to z=y\right)$$
30		iman	$$⊢\left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\to z=y\right)\leftrightarrow \neg \left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)$$
31	30	albii	$$⊢\forall z\left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\to z=y\right)\leftrightarrow \forall z\neg \left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)$$
32		alnex	$$⊢\forall z\neg \left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)\leftrightarrow \neg \exists z\left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)$$
33	31 32	bitri	$$⊢\forall z\left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\to z=y\right)\leftrightarrow \neg \exists z\left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)$$
34	33	exbii	$$⊢\exists y\forall z\left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\to z=y\right)\leftrightarrow \exists y\neg \exists z\left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)$$
35		exnal	$$⊢\exists y\neg \exists z\left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)\leftrightarrow \neg \forall y\exists z\left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)$$
36	34 35	bitri	$$⊢\exists y\forall z\left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\to z=y\right)\leftrightarrow \neg \forall y\exists z\left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)$$
37	36	albii	$$⊢\forall x\exists y\forall z\left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\to z=y\right)\leftrightarrow \forall x\neg \forall y\exists z\left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)$$
38		alnex	$$⊢\forall x\neg \forall y\exists z\left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)\leftrightarrow \neg \exists x\forall y\exists z\left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)$$
39	29 37 38	3bitrri	$$⊢\neg \exists x\forall y\exists z\left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)\leftrightarrow \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)$$
40	39	con1bii	$$⊢\neg \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\leftrightarrow \exists x\forall y\exists z\left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)$$
41		sp	$$⊢\forall y\exists z\left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)\to \exists z\left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)$$
42	41	eximi	$$⊢\exists x\forall y\exists z\left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)\to \exists x\exists z\left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)$$
43	40 42	sylbi	$$⊢\neg \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to \exists x\exists z\left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)$$
44		snssi	$$⊢A\in \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to \left\{A\right\}\subseteq \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)$$
45		residm	$$⊢{\left({F\upharpoonright }_{\left\{A\right\}}\right)\upharpoonright }_{\left\{A\right\}}={F\upharpoonright }_{\left\{A\right\}}$$
46	45	dmeqi	$$⊢\mathrm{dom}\left({\left({F\upharpoonright }_{\left\{A\right\}}\right)\upharpoonright }_{\left\{A\right\}}\right)=\mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)$$
47		ssdmres	$$⊢\left\{A\right\}\subseteq \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)\leftrightarrow \mathrm{dom}\left({\left({F\upharpoonright }_{\left\{A\right\}}\right)\upharpoonright }_{\left\{A\right\}}\right)=\left\{A\right\}$$
48	47	biimpi	$$⊢\left\{A\right\}\subseteq \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to \mathrm{dom}\left({\left({F\upharpoonright }_{\left\{A\right\}}\right)\upharpoonright }_{\left\{A\right\}}\right)=\left\{A\right\}$$
49	46 48	syl5eqr	$$⊢\left\{A\right\}\subseteq \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)=\left\{A\right\}$$
50	44 49	syl	$$⊢A\in \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)=\left\{A\right\}$$
51		vex	$$⊢x\in \mathrm{V}$$
52		vex	$$⊢z\in \mathrm{V}$$
53	51 52	breldm	$$⊢x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\to x\in \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)$$
54		eleq2	$$⊢\mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)=\left\{A\right\}\to \left(x\in \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)\leftrightarrow x\in \left\{A\right\}\right)$$
55		velsn	$$⊢x\in \left\{A\right\}\leftrightarrow x=A$$
56	54 55	syl6bb	$$⊢\mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)=\left\{A\right\}\to \left(x\in \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)\leftrightarrow x=A\right)$$
57	56	biimpa	$$⊢\left(\mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)=\left\{A\right\}\wedge x\in \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)\right)\to x=A$$
58	50 53 57	syl2an	$$⊢\left(A\in \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)\wedge x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\right)\to x=A$$
59	58	breq1d	$$⊢\left(A\in \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)\wedge x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\right)\to \left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\leftrightarrow A\left({F\upharpoonright }_{\left\{A\right\}}\right)z\right)$$
60	59	biimpd	$$⊢\left(A\in \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)\wedge x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\right)\to \left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\to A\left({F\upharpoonright }_{\left\{A\right\}}\right)z\right)$$
61	60	ex	$$⊢A\in \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to \left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\to \left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\to A\left({F\upharpoonright }_{\left\{A\right\}}\right)z\right)\right)$$
62	61	pm2.43d	$$⊢A\in \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to \left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\to A\left({F\upharpoonright }_{\left\{A\right\}}\right)z\right)$$
63	62	anim1d	$$⊢A\in \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to \left(\left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)\to \left(A\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)\right)$$
64	63	eximdv	$$⊢A\in \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to \left(\exists z\left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)\to \exists z\left(A\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)\right)$$
65	64	exlimdv	$$⊢A\in \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to \left(\exists x\exists z\left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)\to \exists z\left(A\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)\right)$$
66	43 65	mpan9	$$⊢\left(\neg \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\wedge A\in \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)\right)\to \exists z\left(A\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)$$
67	9	eleq2i	$$⊢y\in \left({F\upharpoonright }_{\left\{A\right\}}\right)\left[\left\{A\right\}\right]\leftrightarrow y\in F\left[\left\{A\right\}\right]$$
68		elimasni	$$⊢y\in \left({F\upharpoonright }_{\left\{A\right\}}\right)\left[\left\{A\right\}\right]\to A\left({F\upharpoonright }_{\left\{A\right\}}\right)y$$
69	67 68	sylbir	$$⊢y\in F\left[\left\{A\right\}\right]\to A\left({F\upharpoonright }_{\left\{A\right\}}\right)y$$
70		vex	$$⊢y\in \mathrm{V}$$
71	70 52	uniop	$$⊢\bigcup ⟨y,z⟩=\left\{y,z\right\}$$
72		opex	$$⊢⟨y,z⟩\in \mathrm{V}$$
73	72	unisn	$$⊢\bigcup \left\{⟨y,z⟩\right\}=⟨y,z⟩$$
74	27	brrelex1i	$$⊢A\left({F\upharpoonright }_{\left\{A\right\}}\right)z\to A\in \mathrm{V}$$
75		brcnvg	$$⊢\left(y\in \mathrm{V}\wedge A\in \mathrm{V}\right)\to \left(y{\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}A\leftrightarrow A\left({F\upharpoonright }_{\left\{A\right\}}\right)y\right)$$
76	70 74 75	sylancr	$$⊢A\left({F\upharpoonright }_{\left\{A\right\}}\right)z\to \left(y{\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}A\leftrightarrow A\left({F\upharpoonright }_{\left\{A\right\}}\right)y\right)$$
77	76	biimpar	$$⊢\left(A\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge A\left({F\upharpoonright }_{\left\{A\right\}}\right)y\right)\to y{\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}A$$
78	74	adantl	$$⊢\left(y{\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}A\wedge A\left({F\upharpoonright }_{\left\{A\right\}}\right)z\right)\to A\in \mathrm{V}$$
79		breq2	$$⊢x=A\to \left(y{\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}x\leftrightarrow y{\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}A\right)$$
80		breq1	$$⊢x=A\to \left(x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\leftrightarrow A\left({F\upharpoonright }_{\left\{A\right\}}\right)z\right)$$
81	79 80	anbi12d	$$⊢x=A\to \left(\left(y{\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}x\wedge x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\right)\leftrightarrow \left(y{\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}A\wedge A\left({F\upharpoonright }_{\left\{A\right\}}\right)z\right)\right)$$
82	81	rspcev	$$⊢\left(A\in \mathrm{V}\wedge \left(y{\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}A\wedge A\left({F\upharpoonright }_{\left\{A\right\}}\right)z\right)\right)\to \exists x\in \mathrm{V}\left(y{\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}x\wedge x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\right)$$
83	78 82	mpancom	$$⊢\left(y{\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}A\wedge A\left({F\upharpoonright }_{\left\{A\right\}}\right)z\right)\to \exists x\in \mathrm{V}\left(y{\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}x\wedge x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\right)$$
84	83	ancoms	$$⊢\left(A\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge y{\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}A\right)\to \exists x\in \mathrm{V}\left(y{\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}x\wedge x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\right)$$
85	77 84	syldan	$$⊢\left(A\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge A\left({F\upharpoonright }_{\left\{A\right\}}\right)y\right)\to \exists x\in \mathrm{V}\left(y{\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}x\wedge x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\right)$$
86	85	anim1i	$$⊢\left(\left(A\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge A\left({F\upharpoonright }_{\left\{A\right\}}\right)y\right)\wedge \neg z=y\right)\to \left(\exists x\in \mathrm{V}\left(y{\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}x\wedge x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\right)\wedge \neg z=y\right)$$
87	86	an32s	$$⊢\left(\left(A\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)\wedge A\left({F\upharpoonright }_{\left\{A\right\}}\right)y\right)\to \left(\exists x\in \mathrm{V}\left(y{\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}x\wedge x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\right)\wedge \neg z=y\right)$$
88		eldif	$$⊢⟨y,z⟩\in \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\leftrightarrow \left(⟨y,z⟩\in \left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\wedge \neg ⟨y,z⟩\in \mathrm{I}\right)$$
89		rexv	$$⊢\exists x\in \mathrm{V}\left(y{\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}x\wedge x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\right)\leftrightarrow \exists x\left(y{\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}x\wedge x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\right)$$
90	70 52	brco	$$⊢y\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)z\leftrightarrow \exists x\left(y{\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}x\wedge x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\right)$$
91		df-br	$$⊢y\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)z\leftrightarrow ⟨y,z⟩\in \left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)$$
92	89 90 91	3bitr2ri	$$⊢⟨y,z⟩\in \left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\leftrightarrow \exists x\in \mathrm{V}\left(y{\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}x\wedge x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\right)$$
93	52	ideq	$$⊢y\mathrm{I}z\leftrightarrow y=z$$
94		df-br	$$⊢y\mathrm{I}z\leftrightarrow ⟨y,z⟩\in \mathrm{I}$$
95		equcom	$$⊢y=z\leftrightarrow z=y$$
96	93 94 95	3bitr3i	$$⊢⟨y,z⟩\in \mathrm{I}\leftrightarrow z=y$$
97	96	notbii	$$⊢\neg ⟨y,z⟩\in \mathrm{I}\leftrightarrow \neg z=y$$
98	92 97	anbi12i	$$⊢\left(⟨y,z⟩\in \left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\wedge \neg ⟨y,z⟩\in \mathrm{I}\right)\leftrightarrow \left(\exists x\in \mathrm{V}\left(y{\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}x\wedge x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\right)\wedge \neg z=y\right)$$
99	88 98	bitr2i	$$⊢\left(\exists x\in \mathrm{V}\left(y{\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}x\wedge x\left({F\upharpoonright }_{\left\{A\right\}}\right)z\right)\wedge \neg z=y\right)\leftrightarrow ⟨y,z⟩\in \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)$$
100	87 99	sylib	$$⊢\left(\left(A\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)\wedge A\left({F\upharpoonright }_{\left\{A\right\}}\right)y\right)\to ⟨y,z⟩\in \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)$$
101		snssi	$$⊢⟨y,z⟩\in \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\to \left\{⟨y,z⟩\right\}\subseteq \left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}$$
102		uniss	$$⊢\left\{⟨y,z⟩\right\}\subseteq \left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\to \bigcup \left\{⟨y,z⟩\right\}\subseteq \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)$$
103	100 101 102	3syl	$$⊢\left(\left(A\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)\wedge A\left({F\upharpoonright }_{\left\{A\right\}}\right)y\right)\to \bigcup \left\{⟨y,z⟩\right\}\subseteq \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)$$
104	73 103	eqsstrrid	$$⊢\left(\left(A\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)\wedge A\left({F\upharpoonright }_{\left\{A\right\}}\right)y\right)\to ⟨y,z⟩\subseteq \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)$$
105	104	unissd	$$⊢\left(\left(A\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)\wedge A\left({F\upharpoonright }_{\left\{A\right\}}\right)y\right)\to \bigcup ⟨y,z⟩\subseteq \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)$$
106	71 105	eqsstrrid	$$⊢\left(\left(A\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)\wedge A\left({F\upharpoonright }_{\left\{A\right\}}\right)y\right)\to \left\{y,z\right\}\subseteq \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)$$
107	70 52	prss	$$⊢\left(y\in \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\wedge z\in \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\right)\leftrightarrow \left\{y,z\right\}\subseteq \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)$$
108	106 107	sylibr	$$⊢\left(\left(A\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)\wedge A\left({F\upharpoonright }_{\left\{A\right\}}\right)y\right)\to \left(y\in \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\wedge z\in \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\right)$$
109	108	simpld	$$⊢\left(\left(A\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)\wedge A\left({F\upharpoonright }_{\left\{A\right\}}\right)y\right)\to y\in \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)$$
110	109	ex	$$⊢\left(A\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)\to \left(A\left({F\upharpoonright }_{\left\{A\right\}}\right)y\to y\in \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\right)$$
111	69 110	syl5	$$⊢\left(A\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)\to \left(y\in F\left[\left\{A\right\}\right]\to y\in \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\right)$$
112	111	exlimiv	$$⊢\exists z\left(A\left({F\upharpoonright }_{\left\{A\right\}}\right)z\wedge \neg z=y\right)\to \left(y\in F\left[\left\{A\right\}\right]\to y\in \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\right)$$
113	66 112	syl	$$⊢\left(\neg \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\wedge A\in \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)\right)\to \left(y\in F\left[\left\{A\right\}\right]\to y\in \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\right)$$
114	113	ssrdv	$$⊢\left(\neg \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\wedge A\in \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)\right)\to F\left[\left\{A\right\}\right]\subseteq \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)$$
115		ssdif0	$$⊢F\left[\left\{A\right\}\right]\subseteq \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\leftrightarrow F\left[\left\{A\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)=\varnothing$$
116	114 115	sylib	$$⊢\left(\neg \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\wedge A\in \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)\right)\to F\left[\left\{A\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)=\varnothing$$
117	116	ex	$$⊢\neg \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to \left(A\in \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to F\left[\left\{A\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)=\varnothing \right)$$
118		ndmima	$$⊢\neg A\in \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to \left({F\upharpoonright }_{\left\{A\right\}}\right)\left[\left\{A\right\}\right]=\varnothing$$
119	9 118	syl5eqr	$$⊢\neg A\in \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to F\left[\left\{A\right\}\right]=\varnothing$$
120	119	difeq1d	$$⊢\neg A\in \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to F\left[\left\{A\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)=\varnothing \setminus \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)$$
121		0dif	$$⊢\varnothing \setminus \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)=\varnothing$$
122	120 121	eqtrdi	$$⊢\neg A\in \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to F\left[\left\{A\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)=\varnothing$$
123	117 122	pm2.61d1	$$⊢\neg \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to F\left[\left\{A\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)=\varnothing$$
124	123	unieqd	$$⊢\neg \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to \bigcup \left(F\left[\left\{A\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\right)=\bigcup \varnothing$$
125	124 17	eqtrdi	$$⊢\neg \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to \bigcup \left(F\left[\left\{A\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\right)=\varnothing$$
126	26 125	eqtr4d	$$⊢\neg \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to F\left(A\right)=\bigcup \left(F\left[\left\{A\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\right)$$
127	25 126	pm2.61i	$$⊢F\left(A\right)=\bigcup \left(F\left[\left\{A\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({F\upharpoonright }_{\left\{A\right\}}\right)\circ {\left({F\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\right)$$