Metamath Proof Explorer

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}↾}_{\bigcup {D}}\right)\cup \left({{{g}}^{-1}↾}_{\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}↾}_{\bigcup {D}}\right)\cup \left({{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)$
4 funres ${⊢}\mathrm{Fun}{f}\to \mathrm{Fun}\left({{f}↾}_{\bigcup {D}}\right)$
5 funres ${⊢}\mathrm{Fun}{{g}}^{-1}\to \mathrm{Fun}\left({{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)$
6 dmres ${⊢}\mathrm{dom}\left({{f}↾}_{\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}↾}_{\bigcup {D}}\right)\subseteq \bigcup {D}$
9 ssrin ${⊢}\mathrm{dom}\left({{f}↾}_{\bigcup {D}}\right)\subseteq \bigcup {D}\to \mathrm{dom}\left({{f}↾}_{\bigcup {D}}\right)\cap \mathrm{dom}\left({{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)\subseteq \bigcup {D}\cap \mathrm{dom}\left({{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)$
10 8 9 ax-mp ${⊢}\mathrm{dom}\left({{f}↾}_{\bigcup {D}}\right)\cap \mathrm{dom}\left({{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)\subseteq \bigcup {D}\cap \mathrm{dom}\left({{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)$
11 dmres ${⊢}\mathrm{dom}\left({{{g}}^{-1}↾}_{\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}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)\subseteq {A}\setminus \bigcup {D}$
14 sslin ${⊢}\mathrm{dom}\left({{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)\subseteq {A}\setminus \bigcup {D}\to \bigcup {D}\cap \mathrm{dom}\left({{{g}}^{-1}↾}_{\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}↾}_{\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}↾}_{\bigcup {D}}\right)\cap \mathrm{dom}\left({{{g}}^{-1}↾}_{\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}↾}_{\bigcup {D}}\right)\cap \mathrm{dom}\left({{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)\subseteq \varnothing$
19 ss0 ${⊢}\mathrm{dom}\left({{f}↾}_{\bigcup {D}}\right)\cap \mathrm{dom}\left({{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)\subseteq \varnothing \to \mathrm{dom}\left({{f}↾}_{\bigcup {D}}\right)\cap \mathrm{dom}\left({{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)=\varnothing$
20 18 19 ax-mp ${⊢}\mathrm{dom}\left({{f}↾}_{\bigcup {D}}\right)\cap \mathrm{dom}\left({{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)=\varnothing$
21 funun ${⊢}\left(\left(\mathrm{Fun}\left({{f}↾}_{\bigcup {D}}\right)\wedge \mathrm{Fun}\left({{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)\right)\wedge \mathrm{dom}\left({{f}↾}_{\bigcup {D}}\right)\cap \mathrm{dom}\left({{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)=\varnothing \right)\to \mathrm{Fun}\left(\left({{f}↾}_{\bigcup {D}}\right)\cup \left({{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)\right)$
22 20 21 mpan2 ${⊢}\left(\mathrm{Fun}\left({{f}↾}_{\bigcup {D}}\right)\wedge \mathrm{Fun}\left({{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)\right)\to \mathrm{Fun}\left(\left({{f}↾}_{\bigcup {D}}\right)\cup \left({{{g}}^{-1}↾}_{\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}↾}_{\bigcup {D}}\right)\cup \left({{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)\right)$
24 3 funeqi ${⊢}\mathrm{Fun}{H}↔\mathrm{Fun}\left(\left({{f}↾}_{\bigcup {D}}\right)\cup \left({{{g}}^{-1}↾}_{\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}$