fthestrcsetc

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 faithful. (Contributed by AV, 2-Apr-2020)

	Ref	Expression
Hypotheses	funcestrcsetc.e	$⊢ E = ExtStrCat (U)$
	funcestrcsetc.s	$⊢ S = SetCat (U)$
	funcestrcsetc.b	$⊢ B = {Base}_{E}$
	funcestrcsetc.c	$⊢ C = {Base}_{S}$
	funcestrcsetc.u	$⊢ φ \to U \in WUni$
	funcestrcsetc.f	$⊢ φ \to F = (x \in B ⟼ {Base}_{x})$
	funcestrcsetc.g	$⊢ φ \to G = (x \in B, y \in B ⟼ {I ↾}_{({Base}_{y}^{{Base}_{x}})})$
Assertion	fthestrcsetc	$⊢ φ \to F (E Faith S) G$

Proof

Step	Hyp	Ref	Expression
1		funcestrcsetc.e	$⊢ E = ExtStrCat (U)$
2		funcestrcsetc.s	$⊢ S = SetCat (U)$
3		funcestrcsetc.b	$⊢ B = {Base}_{E}$
4		funcestrcsetc.c	$⊢ C = {Base}_{S}$
5		funcestrcsetc.u	$⊢ φ \to U \in WUni$
6		funcestrcsetc.f	$⊢ φ \to F = (x \in B ⟼ {Base}_{x})$
7		funcestrcsetc.g	$⊢ φ \to G = (x \in B, y \in B ⟼ {I ↾}_{({Base}_{y}^{{Base}_{x}})})$
8	1 2 3 4 5 6 7	funcestrcsetc	$⊢ φ \to F (E Func S) G$
9	1 2 3 4 5 6 7	funcestrcsetclem8	$⊢ (φ \land (a \in B \land b \in B)) \to (a G b) : a Hom (E) b ⟶ F (a) Hom (S) F (b)$
10	5	adantr	$⊢ (φ \land (a \in B \land b \in B)) \to U \in WUni$
11		eqid	$⊢ Hom (E) = Hom (E)$
12	1 5	estrcbas	$⊢ φ \to U = {Base}_{E}$
13	3 12	eqtr4id	$⊢ φ \to B = U$
14	13	eleq2d	$⊢ φ \to (a \in B \leftrightarrow a \in U)$
15	14	biimpcd	$⊢ a \in B \to (φ \to a \in U)$
16	15	adantr	$⊢ (a \in B \land b \in B) \to (φ \to a \in U)$
17	16	impcom	$⊢ (φ \land (a \in B \land b \in B)) \to a \in U$
18	13	eleq2d	$⊢ φ \to (b \in B \leftrightarrow b \in U)$
19	18	biimpcd	$⊢ b \in B \to (φ \to b \in U)$
20	19	adantl	$⊢ (a \in B \land b \in B) \to (φ \to b \in U)$
21	20	impcom	$⊢ (φ \land (a \in B \land b \in B)) \to b \in U$
22		eqid	$⊢ {Base}_{a} = {Base}_{a}$
23		eqid	$⊢ {Base}_{b} = {Base}_{b}$
24	1 10 11 17 21 22 23	estrchom	$⊢ (φ \land (a \in B \land b \in B)) \to a Hom (E) b = {Base}_{b}^{{Base}_{a}}$
25	24	eleq2d	$⊢ (φ \land (a \in B \land b \in B)) \to (h \in (a Hom (E) b) \leftrightarrow h \in ({Base}_{b}^{{Base}_{a}}))$
26	1 2 3 4 5 6 7 22 23	funcestrcsetclem6	$⊢ (φ \land (a \in B \land b \in B) \land h \in ({Base}_{b}^{{Base}_{a}})) \to (a G b) (h) = h$
27	26	3expia	$⊢ (φ \land (a \in B \land b \in B)) \to (h \in ({Base}_{b}^{{Base}_{a}}) \to (a G b) (h) = h)$
28	25 27	sylbid	$⊢ (φ \land (a \in B \land b \in B)) \to (h \in (a Hom (E) b) \to (a G b) (h) = h)$
29	28	com12	$⊢ h \in (a Hom (E) b) \to ((φ \land (a \in B \land b \in B)) \to (a G b) (h) = h)$
30	29	adantr	$⊢ (h \in (a Hom (E) b) \land k \in (a Hom (E) b)) \to ((φ \land (a \in B \land b \in B)) \to (a G b) (h) = h)$
31	30	impcom	$⊢ ((φ \land (a \in B \land b \in B)) \land (h \in (a Hom (E) b) \land k \in (a Hom (E) b))) \to (a G b) (h) = h$
32	24	eleq2d	$⊢ (φ \land (a \in B \land b \in B)) \to (k \in (a Hom (E) b) \leftrightarrow k \in ({Base}_{b}^{{Base}_{a}}))$
33	1 2 3 4 5 6 7 22 23	funcestrcsetclem6	$⊢ (φ \land (a \in B \land b \in B) \land k \in ({Base}_{b}^{{Base}_{a}})) \to (a G b) (k) = k$
34	33	3expia	$⊢ (φ \land (a \in B \land b \in B)) \to (k \in ({Base}_{b}^{{Base}_{a}}) \to (a G b) (k) = k)$
35	32 34	sylbid	$⊢ (φ \land (a \in B \land b \in B)) \to (k \in (a Hom (E) b) \to (a G b) (k) = k)$
36	35	com12	$⊢ k \in (a Hom (E) b) \to ((φ \land (a \in B \land b \in B)) \to (a G b) (k) = k)$
37	36	adantl	$⊢ (h \in (a Hom (E) b) \land k \in (a Hom (E) b)) \to ((φ \land (a \in B \land b \in B)) \to (a G b) (k) = k)$
38	37	impcom	$⊢ ((φ \land (a \in B \land b \in B)) \land (h \in (a Hom (E) b) \land k \in (a Hom (E) b))) \to (a G b) (k) = k$
39	31 38	eqeq12d	$⊢ ((φ \land (a \in B \land b \in B)) \land (h \in (a Hom (E) b) \land k \in (a Hom (E) b))) \to ((a G b) (h) = (a G b) (k) \leftrightarrow h = k)$
40	39	biimpd	$⊢ ((φ \land (a \in B \land b \in B)) \land (h \in (a Hom (E) b) \land k \in (a Hom (E) b))) \to ((a G b) (h) = (a G b) (k) \to h = k)$
41	40	ralrimivva	$⊢ (φ \land (a \in B \land b \in B)) \to \forall h \in (a Hom (E) b) \forall k \in (a Hom (E) b) ((a G b) (h) = (a G b) (k) \to h = k)$
42		dff13	$⊢ (a G b) : a Hom (E) b \underset{1-1}{⟶} F (a) Hom (S) F (b) \leftrightarrow ((a G b) : a Hom (E) b ⟶ F (a) Hom (S) F (b) \land \forall h \in (a Hom (E) b) \forall k \in (a Hom (E) b) ((a G b) (h) = (a G b) (k) \to h = k))$
43	9 41 42	sylanbrc	$⊢ (φ \land (a \in B \land b \in B)) \to (a G b) : a Hom (E) b \underset{1-1}{⟶} F (a) Hom (S) F (b)$
44	43	ralrimivva	$⊢ φ \to \forall a \in B \forall b \in B (a G b) : a Hom (E) b \underset{1-1}{⟶} F (a) Hom (S) F (b)$
45		eqid	$⊢ Hom (S) = Hom (S)$
46	3 11 45	isfth2	$⊢ F (E Faith S) G \leftrightarrow (F (E Func S) G \land \forall a \in B \forall b \in B (a G b) : a Hom (E) b \underset{1-1}{⟶} F (a) Hom (S) F (b))$
47	8 44 46	sylanbrc	$⊢ φ \to F (E Faith S) G$

Metamath Proof Explorer

Theorem fthestrcsetc

Proof