Theorem sbthlem5

Description: Lemma for sbth . (Contributed by NM, 22-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	sbthlem5	$$⊢\left(\mathrm{dom}f=A\wedge \mathrm{ran}g\subseteq A\right)\to \mathrm{dom}H=A$$

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	1 2	sbthlem1	$$⊢\bigcup D\subseteq A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]$$
5		difss	$$⊢A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\subseteq A$$
6	4 5	sstri	$$⊢\bigcup D\subseteq A$$
7		sseq2	$$⊢\mathrm{dom}f=A\to \left(\bigcup D\subseteq \mathrm{dom}f\leftrightarrow \bigcup D\subseteq A\right)$$
8	6 7	mpbiri	$$⊢\mathrm{dom}f=A\to \bigcup D\subseteq \mathrm{dom}f$$
9		dfss	$$⊢\bigcup D\subseteq \mathrm{dom}f\leftrightarrow \bigcup D=\bigcup D\cap \mathrm{dom}f$$
10	8 9	sylib	$$⊢\mathrm{dom}f=A\to \bigcup D=\bigcup D\cap \mathrm{dom}f$$
11	10	uneq1d	$$⊢\mathrm{dom}f=A\to \bigcup D\cup \left(A\setminus \bigcup D\right)=\left(\bigcup D\cap \mathrm{dom}f\right)\cup \left(A\setminus \bigcup D\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		imassrn	$$⊢g\left[B\setminus f\left[\bigcup D\right]\right]\subseteq \mathrm{ran}g$$
14	12 13	eqsstrrdi	$$⊢\mathrm{ran}g\subseteq A\to A\setminus \bigcup D\subseteq \mathrm{ran}g$$
15		dfss	$$⊢A\setminus \bigcup D\subseteq \mathrm{ran}g\leftrightarrow A\setminus \bigcup D=\left(A\setminus \bigcup D\right)\cap \mathrm{ran}g$$
16	14 15	sylib	$$⊢\mathrm{ran}g\subseteq A\to A\setminus \bigcup D=\left(A\setminus \bigcup D\right)\cap \mathrm{ran}g$$
17	16	uneq2d	$$⊢\mathrm{ran}g\subseteq A\to \left(\bigcup D\cap \mathrm{dom}f\right)\cup \left(A\setminus \bigcup D\right)=\left(\bigcup D\cap \mathrm{dom}f\right)\cup \left(\left(A\setminus \bigcup D\right)\cap \mathrm{ran}g\right)$$
18	11 17	sylan9eq	$$⊢\left(\mathrm{dom}f=A\wedge \mathrm{ran}g\subseteq A\right)\to \bigcup D\cup \left(A\setminus \bigcup D\right)=\left(\bigcup D\cap \mathrm{dom}f\right)\cup \left(\left(A\setminus \bigcup D\right)\cap \mathrm{ran}g\right)$$
19	3	dmeqi	$$⊢\mathrm{dom}H=\mathrm{dom}\left(\left({f\upharpoonright }_{\bigcup D}\right)\cup \left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)\right)$$
20		dmun	$$⊢\mathrm{dom}\left(\left({f\upharpoonright }_{\bigcup D}\right)\cup \left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)\right)=\mathrm{dom}\left({f\upharpoonright }_{\bigcup D}\right)\cup \mathrm{dom}\left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)$$
21		dmres	$$⊢\mathrm{dom}\left({f\upharpoonright }_{\bigcup D}\right)=\bigcup D\cap \mathrm{dom}f$$
22		dmres	$$⊢\mathrm{dom}\left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)=\left(A\setminus \bigcup D\right)\cap \mathrm{dom}{g}^{-1}$$
23		df-rn	$$⊢\mathrm{ran}g=\mathrm{dom}{g}^{-1}$$
24	23	eqcomi	$$⊢\mathrm{dom}{g}^{-1}=\mathrm{ran}g$$
25	24	ineq2i	$$⊢\left(A\setminus \bigcup D\right)\cap \mathrm{dom}{g}^{-1}=\left(A\setminus \bigcup D\right)\cap \mathrm{ran}g$$
26	22 25	eqtri	$$⊢\mathrm{dom}\left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)=\left(A\setminus \bigcup D\right)\cap \mathrm{ran}g$$
27	21 26	uneq12i	$$⊢\mathrm{dom}\left({f\upharpoonright }_{\bigcup D}\right)\cup \mathrm{dom}\left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)=\left(\bigcup D\cap \mathrm{dom}f\right)\cup \left(\left(A\setminus \bigcup D\right)\cap \mathrm{ran}g\right)$$
28	20 27	eqtri	$$⊢\mathrm{dom}\left(\left({f\upharpoonright }_{\bigcup D}\right)\cup \left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)\right)=\left(\bigcup D\cap \mathrm{dom}f\right)\cup \left(\left(A\setminus \bigcup D\right)\cap \mathrm{ran}g\right)$$
29	19 28	eqtri	$$⊢\mathrm{dom}H=\left(\bigcup D\cap \mathrm{dom}f\right)\cup \left(\left(A\setminus \bigcup D\right)\cap \mathrm{ran}g\right)$$
30	18 29	syl6reqr	$$⊢\left(\mathrm{dom}f=A\wedge \mathrm{ran}g\subseteq A\right)\to \mathrm{dom}H=\bigcup D\cup \left(A\setminus \bigcup D\right)$$
31		undif	$$⊢\bigcup D\subseteq A\leftrightarrow \bigcup D\cup \left(A\setminus \bigcup D\right)=A$$
32	6 31	mpbi	$$⊢\bigcup D\cup \left(A\setminus \bigcup D\right)=A$$
33	30 32	syl6eq	$$⊢\left(\mathrm{dom}f=A\wedge \mathrm{ran}g\subseteq A\right)\to \mathrm{dom}H=A$$