Theorem sbthlem7

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	sbthlem7	$$⊢\left(\mathrm{Fun}f\wedge \mathrm{Fun}{g}^{-1}\right)\to \mathrm{Fun}H$$

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		funres	$$⊢\mathrm{Fun}f\to \mathrm{Fun}\left({f\upharpoonright }_{\bigcup D}\right)$$
5		funres	$$⊢\mathrm{Fun}{g}^{-1}\to \mathrm{Fun}\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		inss1	$$⊢\bigcup D\cap \mathrm{dom}f\subseteq \bigcup D$$
8	6 7	eqsstri	$$⊢\mathrm{dom}\left({f\upharpoonright }_{\bigcup D}\right)\subseteq \bigcup D$$
9		ssrin	$$⊢\mathrm{dom}\left({f\upharpoonright }_{\bigcup D}\right)\subseteq \bigcup D\to \mathrm{dom}\left({f\upharpoonright }_{\bigcup D}\right)\cap \mathrm{dom}\left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)\subseteq \bigcup D\cap \mathrm{dom}\left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)$$
10	8 9	ax-mp	$$⊢\mathrm{dom}\left({f\upharpoonright }_{\bigcup D}\right)\cap \mathrm{dom}\left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)\subseteq \bigcup D\cap \mathrm{dom}\left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)$$
11		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}$$
12		inss1	$$⊢\left(A\setminus \bigcup D\right)\cap \mathrm{dom}{g}^{-1}\subseteq A\setminus \bigcup D$$
13	11 12	eqsstri	$$⊢\mathrm{dom}\left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)\subseteq A\setminus \bigcup D$$
14		sslin	$$⊢\mathrm{dom}\left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)\subseteq A\setminus \bigcup D\to \bigcup D\cap \mathrm{dom}\left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)\subseteq \bigcup D\cap \left(A\setminus \bigcup D\right)$$
15	13 14	ax-mp	$$⊢\bigcup D\cap \mathrm{dom}\left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)\subseteq \bigcup D\cap \left(A\setminus \bigcup D\right)$$
16	10 15	sstri	$$⊢\mathrm{dom}\left({f\upharpoonright }_{\bigcup D}\right)\cap \mathrm{dom}\left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)\subseteq \bigcup D\cap \left(A\setminus \bigcup D\right)$$
17		disjdif	$$⊢\bigcup D\cap \left(A\setminus \bigcup D\right)=\varnothing$$
18	16 17	sseqtri	$$⊢\mathrm{dom}\left({f\upharpoonright }_{\bigcup D}\right)\cap \mathrm{dom}\left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)\subseteq \varnothing$$
19		ss0	$$⊢\mathrm{dom}\left({f\upharpoonright }_{\bigcup D}\right)\cap \mathrm{dom}\left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)\subseteq \varnothing \to \mathrm{dom}\left({f\upharpoonright }_{\bigcup D}\right)\cap \mathrm{dom}\left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)=\varnothing$$
20	18 19	ax-mp	$$⊢\mathrm{dom}\left({f\upharpoonright }_{\bigcup D}\right)\cap \mathrm{dom}\left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)=\varnothing$$
21		funun	$$⊢\left(\left(\mathrm{Fun}\left({f\upharpoonright }_{\bigcup D}\right)\wedge \mathrm{Fun}\left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)\right)\wedge \mathrm{dom}\left({f\upharpoonright }_{\bigcup D}\right)\cap \mathrm{dom}\left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)=\varnothing \right)\to \mathrm{Fun}\left(\left({f\upharpoonright }_{\bigcup D}\right)\cup \left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)\right)$$
22	20 21	mpan2	$$⊢\left(\mathrm{Fun}\left({f\upharpoonright }_{\bigcup D}\right)\wedge \mathrm{Fun}\left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)\right)\to \mathrm{Fun}\left(\left({f\upharpoonright }_{\bigcup D}\right)\cup \left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)\right)$$
23	4 5 22	syl2an	$$⊢\left(\mathrm{Fun}f\wedge \mathrm{Fun}{g}^{-1}\right)\to \mathrm{Fun}\left(\left({f\upharpoonright }_{\bigcup D}\right)\cup \left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)\right)$$
24	3	funeqi	$$⊢\mathrm{Fun}H\leftrightarrow \mathrm{Fun}\left(\left({f\upharpoonright }_{\bigcup D}\right)\cup \left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)\right)$$
25	23 24	sylibr	$$⊢\left(\mathrm{Fun}f\wedge \mathrm{Fun}{g}^{-1}\right)\to \mathrm{Fun}H$$