Theorem sbthlem2

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\}$$
Assertion	sbthlem2	$$⊢\mathrm{ran}g\subseteq A\to A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\subseteq \bigcup D$$

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	1 2	sbthlem1	$$⊢\bigcup D\subseteq A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]$$
4		imass2	$$⊢\bigcup D\subseteq A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\to f\left[\bigcup D\right]\subseteq f\left[A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right]$$
5		sscon	$$⊢f\left[\bigcup D\right]\subseteq f\left[A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right]\to B\setminus f\left[A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right]\subseteq B\setminus f\left[\bigcup D\right]$$
6	3 4 5	mp2b	$$⊢B\setminus f\left[A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right]\subseteq B\setminus f\left[\bigcup D\right]$$
7		imass2	$$⊢B\setminus f\left[A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right]\subseteq B\setminus f\left[\bigcup D\right]\to g\left[B\setminus f\left[A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right]\right]\subseteq g\left[B\setminus f\left[\bigcup D\right]\right]$$
8		sscon	$$⊢g\left[B\setminus f\left[A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right]\right]\subseteq g\left[B\setminus f\left[\bigcup D\right]\right]\to A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\subseteq A\setminus g\left[B\setminus f\left[A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right]\right]$$
9	6 7 8	mp2b	$$⊢A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\subseteq A\setminus g\left[B\setminus f\left[A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right]\right]$$
10		imassrn	$$⊢g\left[B\setminus f\left[A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right]\right]\subseteq \mathrm{ran}g$$
11		sstr2	$$⊢g\left[B\setminus f\left[A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right]\right]\subseteq \mathrm{ran}g\to \left(\mathrm{ran}g\subseteq A\to g\left[B\setminus f\left[A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right]\right]\subseteq A\right)$$
12	10 11	ax-mp	$$⊢\mathrm{ran}g\subseteq A\to g\left[B\setminus f\left[A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right]\right]\subseteq A$$
13		difss	$$⊢A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\subseteq A$$
14		ssconb	$$⊢\left(g\left[B\setminus f\left[A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right]\right]\subseteq A\wedge A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\subseteq A\right)\to \left(g\left[B\setminus f\left[A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right]\right]\subseteq A\setminus \left(A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right)\leftrightarrow A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\subseteq A\setminus g\left[B\setminus f\left[A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right]\right]\right)$$
15	12 13 14	sylancl	$$⊢\mathrm{ran}g\subseteq A\to \left(g\left[B\setminus f\left[A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right]\right]\subseteq A\setminus \left(A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right)\leftrightarrow A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\subseteq A\setminus g\left[B\setminus f\left[A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right]\right]\right)$$
16	9 15	mpbiri	$$⊢\mathrm{ran}g\subseteq A\to g\left[B\setminus f\left[A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right]\right]\subseteq A\setminus \left(A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right)$$
17	16 13	jctil	$$⊢\mathrm{ran}g\subseteq A\to \left(A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\subseteq A\wedge g\left[B\setminus f\left[A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right]\right]\subseteq A\setminus \left(A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right)\right)$$
18	1	difexi	$$⊢A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\in \mathrm{V}$$
19		sseq1	$$⊢x=A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\to \left(x\subseteq A\leftrightarrow A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\subseteq A\right)$$
20		imaeq2	$$⊢x=A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\to f\left[x\right]=f\left[A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right]$$
21	20	difeq2d	$$⊢x=A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\to B\setminus f\left[x\right]=B\setminus f\left[A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right]$$
22	21	imaeq2d	$$⊢x=A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\to g\left[B\setminus f\left[x\right]\right]=g\left[B\setminus f\left[A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right]\right]$$
23		difeq2	$$⊢x=A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\to A\setminus x=A\setminus \left(A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right)$$
24	22 23	sseq12d	$$⊢x=A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\to \left(g\left[B\setminus f\left[x\right]\right]\subseteq A\setminus x\leftrightarrow g\left[B\setminus f\left[A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right]\right]\subseteq A\setminus \left(A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right)\right)$$
25	19 24	anbi12d	$$⊢x=A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\to \left(\left(x\subseteq A\wedge g\left[B\setminus f\left[x\right]\right]\subseteq A\setminus x\right)\leftrightarrow \left(A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\subseteq A\wedge g\left[B\setminus f\left[A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right]\right]\subseteq A\setminus \left(A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right)\right)\right)$$
26	18 25	elab	$$⊢A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\in \left\{x|\left(x\subseteq A\wedge g\left[B\setminus f\left[x\right]\right]\subseteq A\setminus x\right)\right\}\leftrightarrow \left(A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\subseteq A\wedge g\left[B\setminus f\left[A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right]\right]\subseteq A\setminus \left(A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\right)\right)$$
27	17 26	sylibr	$$⊢\mathrm{ran}g\subseteq A\to A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\in \left\{x|\left(x\subseteq A\wedge g\left[B\setminus f\left[x\right]\right]\subseteq A\setminus x\right)\right\}$$
28	27 2	eleqtrrdi	$$⊢\mathrm{ran}g\subseteq A\to A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\in D$$
29		elssuni	$$⊢A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\in D\to A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\subseteq \bigcup D$$
30	28 29	syl	$$⊢\mathrm{ran}g\subseteq A\to A\setminus g\left[B\setminus f\left[\bigcup D\right]\right]\subseteq \bigcup D$$