Theorem sbthlem4

Description: Lemma for sbth . (Contributed by NM, 27-Mar-1998)

	Ref	Expression
Hypotheses	sbthlem.1	$$⊢A\in \mathrm{V}$$
	sbthlem.2	$$⊢D=\left\{x|\left(x\subseteq A\wedge g\left[B\setminus f\left[x\right]\right]\subseteq A\setminus x\right)\right\}$$
Assertion	sbthlem4	$$⊢\left(\left(\mathrm{dom}g=B\wedge \mathrm{ran}g\subseteq A\right)\wedge \mathrm{Fun}{g}^{-1}\right)\to g^{-1}\left[A\setminus \bigcup D\right]=B\setminus f\left[\bigcup D\right]$$

Proof

Step	Hyp	Ref	Expression
1		sbthlem.1	$$⊢A\in \mathrm{V}$$
2		sbthlem.2	$$⊢D=\left\{x|\left(x\subseteq A\wedge g\left[B\setminus f\left[x\right]\right]\subseteq A\setminus x\right)\right\}$$
3		df-ima	$$⊢g^{-1}\left[A\setminus \bigcup D\right]=\mathrm{ran}\left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)$$
4		difss	$$⊢B\setminus f\left[\bigcup D\right]\subseteq B$$
5		sseq2	$$⊢\mathrm{dom}g=B\to \left(B\setminus f\left[\bigcup D\right]\subseteq \mathrm{dom}g\leftrightarrow B\setminus f\left[\bigcup D\right]\subseteq B\right)$$
6	4 5	mpbiri	$$⊢\mathrm{dom}g=B\to B\setminus f\left[\bigcup D\right]\subseteq \mathrm{dom}g$$
7		ssdmres	$$⊢B\setminus f\left[\bigcup D\right]\subseteq \mathrm{dom}g\leftrightarrow \mathrm{dom}\left({g\upharpoonright }_{\left(B\setminus f\left[\bigcup D\right]\right)}\right)=B\setminus f\left[\bigcup D\right]$$
8	6 7	sylib	$$⊢\mathrm{dom}g=B\to \mathrm{dom}\left({g\upharpoonright }_{\left(B\setminus f\left[\bigcup D\right]\right)}\right)=B\setminus f\left[\bigcup D\right]$$
9		dfdm4	$$⊢\mathrm{dom}\left({g\upharpoonright }_{\left(B\setminus f\left[\bigcup D\right]\right)}\right)=\mathrm{ran}{\left({g\upharpoonright }_{\left(B\setminus f\left[\bigcup D\right]\right)}\right)}^{-1}$$
10	8 9	eqtr3di	$$⊢\mathrm{dom}g=B\to B\setminus f\left[\bigcup D\right]=\mathrm{ran}{\left({g\upharpoonright }_{\left(B\setminus f\left[\bigcup D\right]\right)}\right)}^{-1}$$
11		funcnvres	$$⊢\mathrm{Fun}{g}^{-1}\to {\left({g\upharpoonright }_{\left(B\setminus f\left[\bigcup D\right]\right)}\right)}^{-1}={g^{-1}\upharpoonright }_{g\left[B\setminus f\left[\bigcup D\right]\right]}$$
12	1 2	sbthlem3	$$⊢\mathrm{ran}g\subseteq A\to g\left[B\setminus f\left[\bigcup D\right]\right]=A\setminus \bigcup D$$
13	12	reseq2d	$$⊢\mathrm{ran}g\subseteq A\to {g^{-1}\upharpoonright }_{g\left[B\setminus f\left[\bigcup D\right]\right]}={g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}$$
14	11 13	sylan9eqr	$$⊢\left(\mathrm{ran}g\subseteq A\wedge \mathrm{Fun}{g}^{-1}\right)\to {\left({g\upharpoonright }_{\left(B\setminus f\left[\bigcup D\right]\right)}\right)}^{-1}={g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}$$
15	14	rneqd	$$⊢\left(\mathrm{ran}g\subseteq A\wedge \mathrm{Fun}{g}^{-1}\right)\to \mathrm{ran}{\left({g\upharpoonright }_{\left(B\setminus f\left[\bigcup D\right]\right)}\right)}^{-1}=\mathrm{ran}\left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)$$
16	10 15	sylan9eq	$$⊢\left(\mathrm{dom}g=B\wedge \left(\mathrm{ran}g\subseteq A\wedge \mathrm{Fun}{g}^{-1}\right)\right)\to B\setminus f\left[\bigcup D\right]=\mathrm{ran}\left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)$$
17	16	anassrs	$$⊢\left(\left(\mathrm{dom}g=B\wedge \mathrm{ran}g\subseteq A\right)\wedge \mathrm{Fun}{g}^{-1}\right)\to B\setminus f\left[\bigcup D\right]=\mathrm{ran}\left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)$$
18	3 17	eqtr4id	$$⊢\left(\left(\mathrm{dom}g=B\wedge \mathrm{ran}g\subseteq A\right)\wedge \mathrm{Fun}{g}^{-1}\right)\to g^{-1}\left[A\setminus \bigcup D\right]=B\setminus f\left[\bigcup D\right]$$