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