# Metamath Proof Explorer

## Theorem equivestrcsetc

Description: The "natural forgetful functor" from the category of extensible structures into the category of sets which sends each extensible structure to its base set is an equivalence. According to definition 3.33 (1) of Adamek p. 36, "A functor F : A -> B is called an equivalence provided that it is full, faithful, and isomorphism-dense in the sense that for any B-object B' there exists some A-object A' such that F(A') is isomorphic to B'.". Therefore, the category of sets and the category of extensible structures are equivalent, according to definition 3.33 (2) of Adamek p. 36, "Categories A and B are called equivalent provided that there is an equivalence from A to B.". (Contributed by AV, 2-Apr-2020)

Ref Expression
Hypotheses funcestrcsetc.e ${⊢}{E}=\mathrm{ExtStrCat}\left({U}\right)$
funcestrcsetc.s ${⊢}{S}=\mathrm{SetCat}\left({U}\right)$
funcestrcsetc.b ${⊢}{B}={\mathrm{Base}}_{{E}}$
funcestrcsetc.c ${⊢}{C}={\mathrm{Base}}_{{S}}$
funcestrcsetc.u ${⊢}{\phi }\to {U}\in \mathrm{WUni}$
funcestrcsetc.f ${⊢}{\phi }\to {F}=\left({x}\in {B}⟼{\mathrm{Base}}_{{x}}\right)$
funcestrcsetc.g ${⊢}{\phi }\to {G}=\left({x}\in {B},{y}\in {B}⟼{\mathrm{I}↾}_{\left({{\mathrm{Base}}_{{y}}}^{{\mathrm{Base}}_{{x}}}\right)}\right)$
equivestrcsetc.i ${⊢}{\phi }\to {\mathrm{Base}}_{\mathrm{ndx}}\in {U}$
Assertion equivestrcsetc ${⊢}{\phi }\to \left({F}\left({E}\mathrm{Faith}{S}\right){G}\wedge {F}\left({E}\mathrm{Full}{S}\right){G}\wedge \forall {b}\in {C}\phantom{\rule{.4em}{0ex}}\exists {a}\in {B}\phantom{\rule{.4em}{0ex}}\exists {i}\phantom{\rule{.4em}{0ex}}{i}:{b}\underset{1-1 onto}{⟶}{F}\left({a}\right)\right)$

### Proof

Step Hyp Ref Expression
1 funcestrcsetc.e ${⊢}{E}=\mathrm{ExtStrCat}\left({U}\right)$
2 funcestrcsetc.s ${⊢}{S}=\mathrm{SetCat}\left({U}\right)$
3 funcestrcsetc.b ${⊢}{B}={\mathrm{Base}}_{{E}}$
4 funcestrcsetc.c ${⊢}{C}={\mathrm{Base}}_{{S}}$
5 funcestrcsetc.u ${⊢}{\phi }\to {U}\in \mathrm{WUni}$
6 funcestrcsetc.f ${⊢}{\phi }\to {F}=\left({x}\in {B}⟼{\mathrm{Base}}_{{x}}\right)$
7 funcestrcsetc.g ${⊢}{\phi }\to {G}=\left({x}\in {B},{y}\in {B}⟼{\mathrm{I}↾}_{\left({{\mathrm{Base}}_{{y}}}^{{\mathrm{Base}}_{{x}}}\right)}\right)$
8 equivestrcsetc.i ${⊢}{\phi }\to {\mathrm{Base}}_{\mathrm{ndx}}\in {U}$
9 1 2 3 4 5 6 7 fthestrcsetc ${⊢}{\phi }\to {F}\left({E}\mathrm{Faith}{S}\right){G}$
10 1 2 3 4 5 6 7 fullestrcsetc ${⊢}{\phi }\to {F}\left({E}\mathrm{Full}{S}\right){G}$
11 2 5 setcbas ${⊢}{\phi }\to {U}={\mathrm{Base}}_{{S}}$
12 11 4 syl6reqr ${⊢}{\phi }\to {C}={U}$
13 12 eleq2d ${⊢}{\phi }\to \left({b}\in {C}↔{b}\in {U}\right)$
14 eqid ${⊢}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩\right\}$
15 14 5 8 1strwunbndx ${⊢}\left({\phi }\wedge {b}\in {U}\right)\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩\right\}\in {U}$
16 15 ex ${⊢}{\phi }\to \left({b}\in {U}\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩\right\}\in {U}\right)$
17 13 16 sylbid ${⊢}{\phi }\to \left({b}\in {C}\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩\right\}\in {U}\right)$
18 17 imp ${⊢}\left({\phi }\wedge {b}\in {C}\right)\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩\right\}\in {U}$
19 1 5 estrcbas ${⊢}{\phi }\to {U}={\mathrm{Base}}_{{E}}$
20 19 adantr ${⊢}\left({\phi }\wedge {b}\in {C}\right)\to {U}={\mathrm{Base}}_{{E}}$
21 20 3 syl6reqr ${⊢}\left({\phi }\wedge {b}\in {C}\right)\to {B}={U}$
22 18 21 eleqtrrd ${⊢}\left({\phi }\wedge {b}\in {C}\right)\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩\right\}\in {B}$
23 fveq2 ${⊢}{a}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩\right\}\to {F}\left({a}\right)={F}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩\right\}\right)$
24 23 f1oeq3d ${⊢}{a}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩\right\}\to \left({i}:{b}\underset{1-1 onto}{⟶}{F}\left({a}\right)↔{i}:{b}\underset{1-1 onto}{⟶}{F}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩\right\}\right)\right)$
25 24 exbidv ${⊢}{a}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩\right\}\to \left(\exists {i}\phantom{\rule{.4em}{0ex}}{i}:{b}\underset{1-1 onto}{⟶}{F}\left({a}\right)↔\exists {i}\phantom{\rule{.4em}{0ex}}{i}:{b}\underset{1-1 onto}{⟶}{F}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩\right\}\right)\right)$
26 25 adantl ${⊢}\left(\left({\phi }\wedge {b}\in {C}\right)\wedge {a}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩\right\}\right)\to \left(\exists {i}\phantom{\rule{.4em}{0ex}}{i}:{b}\underset{1-1 onto}{⟶}{F}\left({a}\right)↔\exists {i}\phantom{\rule{.4em}{0ex}}{i}:{b}\underset{1-1 onto}{⟶}{F}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩\right\}\right)\right)$
27 f1oi ${⊢}\left({\mathrm{I}↾}_{{b}}\right):{b}\underset{1-1 onto}{⟶}{b}$
28 1 2 3 4 5 6 funcestrcsetclem1 ${⊢}\left({\phi }\wedge \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩\right\}\in {B}\right)\to {F}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩\right\}\right)={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩\right\}}$
29 22 28 syldan ${⊢}\left({\phi }\wedge {b}\in {C}\right)\to {F}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩\right\}\right)={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩\right\}}$
30 14 1strbas ${⊢}{b}\in {C}\to {b}={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩\right\}}$
31 30 adantl ${⊢}\left({\phi }\wedge {b}\in {C}\right)\to {b}={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩\right\}}$
32 29 31 eqtr4d ${⊢}\left({\phi }\wedge {b}\in {C}\right)\to {F}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩\right\}\right)={b}$
33 32 f1oeq3d ${⊢}\left({\phi }\wedge {b}\in {C}\right)\to \left(\left({\mathrm{I}↾}_{{b}}\right):{b}\underset{1-1 onto}{⟶}{F}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩\right\}\right)↔\left({\mathrm{I}↾}_{{b}}\right):{b}\underset{1-1 onto}{⟶}{b}\right)$
34 27 33 mpbiri ${⊢}\left({\phi }\wedge {b}\in {C}\right)\to \left({\mathrm{I}↾}_{{b}}\right):{b}\underset{1-1 onto}{⟶}{F}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩\right\}\right)$
35 resiexg ${⊢}{b}\in \mathrm{V}\to {\mathrm{I}↾}_{{b}}\in \mathrm{V}$
36 35 elv ${⊢}{\mathrm{I}↾}_{{b}}\in \mathrm{V}$
37 f1oeq1 ${⊢}{i}={\mathrm{I}↾}_{{b}}\to \left({i}:{b}\underset{1-1 onto}{⟶}{F}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩\right\}\right)↔\left({\mathrm{I}↾}_{{b}}\right):{b}\underset{1-1 onto}{⟶}{F}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩\right\}\right)\right)$
38 36 37 spcev ${⊢}\left({\mathrm{I}↾}_{{b}}\right):{b}\underset{1-1 onto}{⟶}{F}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩\right\}\right)\to \exists {i}\phantom{\rule{.4em}{0ex}}{i}:{b}\underset{1-1 onto}{⟶}{F}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩\right\}\right)$
39 34 38 syl ${⊢}\left({\phi }\wedge {b}\in {C}\right)\to \exists {i}\phantom{\rule{.4em}{0ex}}{i}:{b}\underset{1-1 onto}{⟶}{F}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩\right\}\right)$
40 22 26 39 rspcedvd ${⊢}\left({\phi }\wedge {b}\in {C}\right)\to \exists {a}\in {B}\phantom{\rule{.4em}{0ex}}\exists {i}\phantom{\rule{.4em}{0ex}}{i}:{b}\underset{1-1 onto}{⟶}{F}\left({a}\right)$
41 40 ralrimiva ${⊢}{\phi }\to \forall {b}\in {C}\phantom{\rule{.4em}{0ex}}\exists {a}\in {B}\phantom{\rule{.4em}{0ex}}\exists {i}\phantom{\rule{.4em}{0ex}}{i}:{b}\underset{1-1 onto}{⟶}{F}\left({a}\right)$
42 9 10 41 3jca ${⊢}{\phi }\to \left({F}\left({E}\mathrm{Faith}{S}\right){G}\wedge {F}\left({E}\mathrm{Full}{S}\right){G}\wedge \forall {b}\in {C}\phantom{\rule{.4em}{0ex}}\exists {a}\in {B}\phantom{\rule{.4em}{0ex}}\exists {i}\phantom{\rule{.4em}{0ex}}{i}:{b}\underset{1-1 onto}{⟶}{F}\left({a}\right)\right)$