Theorem sbthlem6

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\}$$
	sbthlem.3	$$⊢H=\left({f\upharpoonright }_{\bigcup D}\right)\cup \left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)$$
Assertion	sbthlem6	$$⊢\left(\mathrm{ran}f\subseteq B\wedge \left(\left(\mathrm{dom}g=B\wedge \mathrm{ran}g\subseteq A\right)\wedge \mathrm{Fun}{g}^{-1}\right)\right)\to \mathrm{ran}H=B$$

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		sbthlem.3	$$⊢H=\left({f\upharpoonright }_{\bigcup D}\right)\cup \left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)$$
4		rnun	$$⊢\mathrm{ran}\left(\left({f\upharpoonright }_{\bigcup D}\right)\cup \left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)\right)=\mathrm{ran}\left({f\upharpoonright }_{\bigcup D}\right)\cup \mathrm{ran}\left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)$$
5	3	rneqi	$$⊢\mathrm{ran}H=\mathrm{ran}\left(\left({f\upharpoonright }_{\bigcup D}\right)\cup \left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)\right)$$
6		df-ima	$$⊢f\left[\bigcup D\right]=\mathrm{ran}\left({f\upharpoonright }_{\bigcup D}\right)$$
7	6	uneq1i	$$⊢f\left[\bigcup D\right]\cup \mathrm{ran}\left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)=\mathrm{ran}\left({f\upharpoonright }_{\bigcup D}\right)\cup \mathrm{ran}\left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)$$
8	4 5 7	3eqtr4i	$$⊢\mathrm{ran}H=f\left[\bigcup D\right]\cup \mathrm{ran}\left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)$$
9		df-ima	$$⊢g^{-1}\left[A\setminus \bigcup D\right]=\mathrm{ran}\left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)$$
10	1 2	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]$$
11	9 10	syl5reqr	$$⊢\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)$$
12	11	uneq2d	$$⊢\left(\left(\mathrm{dom}g=B\wedge \mathrm{ran}g\subseteq A\right)\wedge \mathrm{Fun}{g}^{-1}\right)\to f\left[\bigcup D\right]\cup \left(B\setminus f\left[\bigcup D\right]\right)=f\left[\bigcup D\right]\cup \mathrm{ran}\left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)$$
13	8 12	eqtr4id	$$⊢\left(\left(\mathrm{dom}g=B\wedge \mathrm{ran}g\subseteq A\right)\wedge \mathrm{Fun}{g}^{-1}\right)\to \mathrm{ran}H=f\left[\bigcup D\right]\cup \left(B\setminus f\left[\bigcup D\right]\right)$$
14		imassrn	$$⊢f\left[\bigcup D\right]\subseteq \mathrm{ran}f$$
15		sstr2	$$⊢f\left[\bigcup D\right]\subseteq \mathrm{ran}f\to \left(\mathrm{ran}f\subseteq B\to f\left[\bigcup D\right]\subseteq B\right)$$
16	14 15	ax-mp	$$⊢\mathrm{ran}f\subseteq B\to f\left[\bigcup D\right]\subseteq B$$
17		undif	$$⊢f\left[\bigcup D\right]\subseteq B\leftrightarrow f\left[\bigcup D\right]\cup \left(B\setminus f\left[\bigcup D\right]\right)=B$$
18	16 17	sylib	$$⊢\mathrm{ran}f\subseteq B\to f\left[\bigcup D\right]\cup \left(B\setminus f\left[\bigcup D\right]\right)=B$$
19	13 18	sylan9eqr	$$⊢\left(\mathrm{ran}f\subseteq B\wedge \left(\left(\mathrm{dom}g=B\wedge \mathrm{ran}g\subseteq A\right)\wedge \mathrm{Fun}{g}^{-1}\right)\right)\to \mathrm{ran}H=B$$