fullsetcestrc

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 full. (Contributed by AV, 1-Apr-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	fullsetcestrc	$⊢ φ \to F (S Full 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 (E) = Hom (E)$
12	1 2 3 4 5	funcsetcestrclem2	$⊢ (φ \land a \in C) \to F (a) \in U$
13	12	adantrr	$⊢ (φ \land (a \in C \land b \in C)) \to F (a) \in U$
14	1 2 3 4 5	funcsetcestrclem2	$⊢ (φ \land b \in C) \to F (b) \in U$
15	14	adantrl	$⊢ (φ \land (a \in C \land b \in C)) \to F (b) \in U$
16		eqid	$⊢ {Base}_{F (a)} = {Base}_{F (a)}$
17		eqid	$⊢ {Base}_{F (b)} = {Base}_{F (b)}$
18	7 10 11 13 15 16 17	elestrchom	$⊢ (φ \land (a \in C \land b \in C)) \to (h \in (F (a) Hom (E) F (b)) \leftrightarrow h : {Base}_{F (a)} ⟶ {Base}_{F (b)})$
19	1 2 3	funcsetcestrclem1	$⊢ (φ \land a \in C) \to F (a) = \{⟨{Base}_{ndx}, a⟩\}$
20	19	adantrr	$⊢ (φ \land (a \in C \land b \in C)) \to F (a) = \{⟨{Base}_{ndx}, a⟩\}$
21	20	fveq2d	$⊢ (φ \land (a \in C \land b \in C)) \to {Base}_{F (a)} = {Base}_{\{⟨{Base}_{ndx}, a⟩\}}$
22		eqid	$⊢ \{⟨{Base}_{ndx}, a⟩\} = \{⟨{Base}_{ndx}, a⟩\}$
23	22	1strbas	$⊢ a \in C \to a = {Base}_{\{⟨{Base}_{ndx}, a⟩\}}$
24	23	ad2antrl	$⊢ (φ \land (a \in C \land b \in C)) \to a = {Base}_{\{⟨{Base}_{ndx}, a⟩\}}$
25	21 24	eqtr4d	$⊢ (φ \land (a \in C \land b \in C)) \to {Base}_{F (a)} = a$
26	1 2 3	funcsetcestrclem1	$⊢ (φ \land b \in C) \to F (b) = \{⟨{Base}_{ndx}, b⟩\}$
27	26	adantrl	$⊢ (φ \land (a \in C \land b \in C)) \to F (b) = \{⟨{Base}_{ndx}, b⟩\}$
28	27	fveq2d	$⊢ (φ \land (a \in C \land b \in C)) \to {Base}_{F (b)} = {Base}_{\{⟨{Base}_{ndx}, b⟩\}}$
29		eqid	$⊢ \{⟨{Base}_{ndx}, b⟩\} = \{⟨{Base}_{ndx}, b⟩\}$
30	29	1strbas	$⊢ b \in C \to b = {Base}_{\{⟨{Base}_{ndx}, b⟩\}}$
31	30	ad2antll	$⊢ (φ \land (a \in C \land b \in C)) \to b = {Base}_{\{⟨{Base}_{ndx}, b⟩\}}$
32	28 31	eqtr4d	$⊢ (φ \land (a \in C \land b \in C)) \to {Base}_{F (b)} = b$
33	25 32	feq23d	$⊢ (φ \land (a \in C \land b \in C)) \to (h : {Base}_{F (a)} ⟶ {Base}_{F (b)} \leftrightarrow h : a ⟶ b)$
34		simpr	$⊢ (φ \land (a \in C \land b \in C)) \to (a \in C \land b \in C)$
35	34	ancomd	$⊢ (φ \land (a \in C \land b \in C)) \to (b \in C \land a \in C)$
36		elmapg	$⊢ (b \in C \land a \in C) \to (h \in (b^{a}) \leftrightarrow h : a ⟶ b)$
37	35 36	syl	$⊢ (φ \land (a \in C \land b \in C)) \to (h \in (b^{a}) \leftrightarrow h : a ⟶ b)$
38	37	biimpar	$⊢ ((φ \land (a \in C \land b \in C)) \land h : a ⟶ b) \to h \in (b^{a})$
39		equequ2	$⊢ k = h \to (h = k \leftrightarrow h = h)$
40	39	adantl	$⊢ (((φ \land (a \in C \land b \in C)) \land h : a ⟶ b) \land k = h) \to (h = k \leftrightarrow h = h)$
41		eqidd	$⊢ ((φ \land (a \in C \land b \in C)) \land h : a ⟶ b) \to h = h$
42	38 40 41	rspcedvd	$⊢ ((φ \land (a \in C \land b \in C)) \land h : a ⟶ b) \to \exists k \in (b^{a}) h = k$
43	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$
44	43	3expa	$⊢ ((φ \land (a \in C \land b \in C)) \land k \in (b^{a})) \to (a G b) (k) = k$
45	44	eqeq2d	$⊢ ((φ \land (a \in C \land b \in C)) \land k \in (b^{a})) \to (h = (a G b) (k) \leftrightarrow h = k)$
46	45	rexbidva	$⊢ (φ \land (a \in C \land b \in C)) \to (\exists k \in (b^{a}) h = (a G b) (k) \leftrightarrow \exists k \in (b^{a}) h = k)$
47	46	adantr	$⊢ ((φ \land (a \in C \land b \in C)) \land h : a ⟶ b) \to (\exists k \in (b^{a}) h = (a G b) (k) \leftrightarrow \exists k \in (b^{a}) h = k)$
48	42 47	mpbird	$⊢ ((φ \land (a \in C \land b \in C)) \land h : a ⟶ b) \to \exists k \in (b^{a}) h = (a G b) (k)$
49		eqid	$⊢ Hom (S) = Hom (S)$
50	1 4	setcbas	$⊢ φ \to U = {Base}_{S}$
51	2 50	eqtr4id	$⊢ φ \to C = U$
52	51	eleq2d	$⊢ φ \to (a \in C \leftrightarrow a \in U)$
53	52	biimpcd	$⊢ a \in C \to (φ \to a \in U)$
54	53	adantr	$⊢ (a \in C \land b \in C) \to (φ \to a \in U)$
55	54	impcom	$⊢ (φ \land (a \in C \land b \in C)) \to a \in U$
56	51	eleq2d	$⊢ φ \to (b \in C \leftrightarrow b \in U)$
57	56	biimpcd	$⊢ b \in C \to (φ \to b \in U)$
58	57	adantl	$⊢ (a \in C \land b \in C) \to (φ \to b \in U)$
59	58	impcom	$⊢ (φ \land (a \in C \land b \in C)) \to b \in U$
60	1 10 49 55 59	setchom	$⊢ (φ \land (a \in C \land b \in C)) \to a Hom (S) b = b^{a}$
61	60	rexeqdv	$⊢ (φ \land (a \in C \land b \in C)) \to (\exists k \in (a Hom (S) b) h = (a G b) (k) \leftrightarrow \exists k \in (b^{a}) h = (a G b) (k))$
62	61	adantr	$⊢ ((φ \land (a \in C \land b \in C)) \land h : a ⟶ b) \to (\exists k \in (a Hom (S) b) h = (a G b) (k) \leftrightarrow \exists k \in (b^{a}) h = (a G b) (k))$
63	48 62	mpbird	$⊢ ((φ \land (a \in C \land b \in C)) \land h : a ⟶ b) \to \exists k \in (a Hom (S) b) h = (a G b) (k)$
64	63	ex	$⊢ (φ \land (a \in C \land b \in C)) \to (h : a ⟶ b \to \exists k \in (a Hom (S) b) h = (a G b) (k))$
65	33 64	sylbid	$⊢ (φ \land (a \in C \land b \in C)) \to (h : {Base}_{F (a)} ⟶ {Base}_{F (b)} \to \exists k \in (a Hom (S) b) h = (a G b) (k))$
66	18 65	sylbid	$⊢ (φ \land (a \in C \land b \in C)) \to (h \in (F (a) Hom (E) F (b)) \to \exists k \in (a Hom (S) b) h = (a G b) (k))$
67	66	ralrimiv	$⊢ (φ \land (a \in C \land b \in C)) \to \forall h \in (F (a) Hom (E) F (b)) \exists k \in (a Hom (S) b) h = (a G b) (k)$
68		dffo3	$⊢ (a G b) : a Hom (S) b \underset{onto}{⟶} F (a) Hom (E) F (b) \leftrightarrow ((a G b) : a Hom (S) b ⟶ F (a) Hom (E) F (b) \land \forall h \in (F (a) Hom (E) F (b)) \exists k \in (a Hom (S) b) h = (a G b) (k))$
69	9 67 68	sylanbrc	$⊢ (φ \land (a \in C \land b \in C)) \to (a G b) : a Hom (S) b \underset{onto}{⟶} F (a) Hom (E) F (b)$
70	69	ralrimivva	$⊢ φ \to \forall a \in C \forall b \in C (a G b) : a Hom (S) b \underset{onto}{⟶} F (a) Hom (E) F (b)$
71	2 11 49	isfull2	$⊢ F (S Full 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{onto}{⟶} F (a) Hom (E) F (b))$
72	8 70 71	sylanbrc	$⊢ φ \to F (S Full E) G$

Metamath Proof Explorer

Theorem fullsetcestrc

Proof