Theorem sbthlem10

Description: Lemma for sbth . (Contributed by NM, 28-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)$$
	sbthlem.4	$$⊢B\in \mathrm{V}$$
Assertion	sbthlem10	$$⊢\left(A\preccurlyeq B\wedge B\preccurlyeq A\right)\to A\approx 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		sbthlem.4	$$⊢B\in \mathrm{V}$$
5	4	brdom	$$⊢A\preccurlyeq B\leftrightarrow \exists ff:A\underset{1-1}{⟶}B$$
6	1	brdom	$$⊢B\preccurlyeq A\leftrightarrow \exists gg:B\underset{1-1}{⟶}A$$
7	5 6	anbi12i	$$⊢\left(A\preccurlyeq B\wedge B\preccurlyeq A\right)\leftrightarrow \left(\exists ff:A\underset{1-1}{⟶}B\wedge \exists gg:B\underset{1-1}{⟶}A\right)$$
8		exdistrv	$$⊢\exists f\exists g\left(f:A\underset{1-1}{⟶}B\wedge g:B\underset{1-1}{⟶}A\right)\leftrightarrow \left(\exists ff:A\underset{1-1}{⟶}B\wedge \exists gg:B\underset{1-1}{⟶}A\right)$$
9	7 8	bitr4i	$$⊢\left(A\preccurlyeq B\wedge B\preccurlyeq A\right)\leftrightarrow \exists f\exists g\left(f:A\underset{1-1}{⟶}B\wedge g:B\underset{1-1}{⟶}A\right)$$
10		vex	$$⊢f\in \mathrm{V}$$
11	10	resex	$$⊢{f\upharpoonright }_{\bigcup D}\in \mathrm{V}$$
12		vex	$$⊢g\in \mathrm{V}$$
13	12	cnvex	$$⊢g^{-1}\in \mathrm{V}$$
14	13	resex	$$⊢{g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\in \mathrm{V}$$
15	11 14	unex	$$⊢\left({f\upharpoonright }_{\bigcup D}\right)\cup \left({g^{-1}\upharpoonright }_{\left(A\setminus \bigcup D\right)}\right)\in \mathrm{V}$$
16	3 15	eqeltri	$$⊢H\in \mathrm{V}$$
17	1 2 3	sbthlem9	$$⊢\left(f:A\underset{1-1}{⟶}B\wedge g:B\underset{1-1}{⟶}A\right)\to H:A\underset{1-1\; onto}{⟶}B$$
18		f1oen3g	$$⊢\left(H\in \mathrm{V}\wedge H:A\underset{1-1\; onto}{⟶}B\right)\to A\approx B$$
19	16 17 18	sylancr	$$⊢\left(f:A\underset{1-1}{⟶}B\wedge g:B\underset{1-1}{⟶}A\right)\to A\approx B$$
20	19	exlimivv	$$⊢\exists f\exists g\left(f:A\underset{1-1}{⟶}B\wedge g:B\underset{1-1}{⟶}A\right)\to A\approx B$$
21	9 20	sylbi	$$⊢\left(A\preccurlyeq B\wedge B\preccurlyeq A\right)\to A\approx B$$