fthsetcestrc

Description: The "embedding functor" from the category of sets into the category of extensible structures which sends each set to an extensible structure consisting of the base set slot only is faithful. (Contributed by AV, 31-Mar-2020)

	Ref	Expression
Hypotheses	funcsetcestrc.s	$⊢ S = SetCat (U)$
	funcsetcestrc.c	$⊢ C = {Base}_{S}$
	funcsetcestrc.f	$⊢ φ \to F = (x \in C ⟼ \{⟨{Base}_{ndx}, x⟩\})$
	funcsetcestrc.u	$⊢ φ \to U \in WUni$
	funcsetcestrc.o	$⊢ φ \to ω \in U$
	funcsetcestrc.g	$⊢ φ \to G = (x \in C, y \in C ⟼ {I ↾}_{(y^{x})})$
	funcsetcestrc.e	$⊢ E = ExtStrCat (U)$
Assertion	fthsetcestrc	$⊢ φ \to F (S Faith E) G$

Proof

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

Metamath Proof Explorer

Theorem fthsetcestrc

Proof