fullestrcsetc

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 full. (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	fullestrcsetc	$⊢ φ \to F (E Full 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 (S) = Hom (S)$
12	1 2 3 4 5 6	funcestrcsetclem2	$⊢ (φ \land a \in B) \to F (a) \in U$
13	12	adantrr	$⊢ (φ \land (a \in B \land b \in B)) \to F (a) \in U$
14	1 2 3 4 5 6	funcestrcsetclem2	$⊢ (φ \land b \in B) \to F (b) \in U$
15	14	adantrl	$⊢ (φ \land (a \in B \land b \in B)) \to F (b) \in U$
16	2 10 11 13 15	elsetchom	$⊢ (φ \land (a \in B \land b \in B)) \to (h \in (F (a) Hom (S) F (b)) \leftrightarrow h : F (a) ⟶ F (b))$
17	1 2 3 4 5 6	funcestrcsetclem1	$⊢ (φ \land a \in B) \to F (a) = {Base}_{a}$
18	17	adantrr	$⊢ (φ \land (a \in B \land b \in B)) \to F (a) = {Base}_{a}$
19	1 2 3 4 5 6	funcestrcsetclem1	$⊢ (φ \land b \in B) \to F (b) = {Base}_{b}$
20	19	adantrl	$⊢ (φ \land (a \in B \land b \in B)) \to F (b) = {Base}_{b}$
21	18 20	feq23d	$⊢ (φ \land (a \in B \land b \in B)) \to (h : F (a) ⟶ F (b) \leftrightarrow h : {Base}_{a} ⟶ {Base}_{b})$
22	16 21	bitrd	$⊢ (φ \land (a \in B \land b \in B)) \to (h \in (F (a) Hom (S) F (b)) \leftrightarrow h : {Base}_{a} ⟶ {Base}_{b})$
23		fvex	$⊢ {Base}_{b} \in V$
24		fvex	$⊢ {Base}_{a} \in V$
25	23 24	pm3.2i	$⊢ ({Base}_{b} \in V \land {Base}_{a} \in V)$
26		elmapg	$⊢ ({Base}_{b} \in V \land {Base}_{a} \in V) \to (h \in ({Base}_{b}^{{Base}_{a}}) \leftrightarrow h : {Base}_{a} ⟶ {Base}_{b})$
27	25 26	mp1i	$⊢ (φ \land (a \in B \land b \in B)) \to (h \in ({Base}_{b}^{{Base}_{a}}) \leftrightarrow h : {Base}_{a} ⟶ {Base}_{b})$
28	27	biimpar	$⊢ ((φ \land (a \in B \land b \in B)) \land h : {Base}_{a} ⟶ {Base}_{b}) \to h \in ({Base}_{b}^{{Base}_{a}})$
29		equequ2	$⊢ k = h \to (h = k \leftrightarrow h = h)$
30	29	adantl	$⊢ (((φ \land (a \in B \land b \in B)) \land h : {Base}_{a} ⟶ {Base}_{b}) \land k = h) \to (h = k \leftrightarrow h = h)$
31		eqidd	$⊢ ((φ \land (a \in B \land b \in B)) \land h : {Base}_{a} ⟶ {Base}_{b}) \to h = h$
32	28 30 31	rspcedvd	$⊢ ((φ \land (a \in B \land b \in B)) \land h : {Base}_{a} ⟶ {Base}_{b}) \to \exists k \in ({Base}_{b}^{{Base}_{a}}) h = k$
33		eqid	$⊢ {Base}_{a} = {Base}_{a}$
34		eqid	$⊢ {Base}_{b} = {Base}_{b}$
35	1 2 3 4 5 6 7 33 34	funcestrcsetclem6	$⊢ (φ \land (a \in B \land b \in B) \land k \in ({Base}_{b}^{{Base}_{a}})) \to (a G b) (k) = k$
36	35	3expa	$⊢ ((φ \land (a \in B \land b \in B)) \land k \in ({Base}_{b}^{{Base}_{a}})) \to (a G b) (k) = k$
37	36	eqeq2d	$⊢ ((φ \land (a \in B \land b \in B)) \land k \in ({Base}_{b}^{{Base}_{a}})) \to (h = (a G b) (k) \leftrightarrow h = k)$
38	37	rexbidva	$⊢ (φ \land (a \in B \land b \in B)) \to (\exists k \in ({Base}_{b}^{{Base}_{a}}) h = (a G b) (k) \leftrightarrow \exists k \in ({Base}_{b}^{{Base}_{a}}) h = k)$
39	38	adantr	$⊢ ((φ \land (a \in B \land b \in B)) \land h : {Base}_{a} ⟶ {Base}_{b}) \to (\exists k \in ({Base}_{b}^{{Base}_{a}}) h = (a G b) (k) \leftrightarrow \exists k \in ({Base}_{b}^{{Base}_{a}}) h = k)$
40	32 39	mpbird	$⊢ ((φ \land (a \in B \land b \in B)) \land h : {Base}_{a} ⟶ {Base}_{b}) \to \exists k \in ({Base}_{b}^{{Base}_{a}}) h = (a G b) (k)$
41		eqid	$⊢ Hom (E) = Hom (E)$
42	1 5	estrcbas	$⊢ φ \to U = {Base}_{E}$
43	3 42	eqtr4id	$⊢ φ \to B = U$
44	43	eleq2d	$⊢ φ \to (a \in B \leftrightarrow a \in U)$
45	44	biimpcd	$⊢ a \in B \to (φ \to a \in U)$
46	45	adantr	$⊢ (a \in B \land b \in B) \to (φ \to a \in U)$
47	46	impcom	$⊢ (φ \land (a \in B \land b \in B)) \to a \in U$
48	43	eleq2d	$⊢ φ \to (b \in B \leftrightarrow b \in U)$
49	48	biimpcd	$⊢ b \in B \to (φ \to b \in U)$
50	49	adantl	$⊢ (a \in B \land b \in B) \to (φ \to b \in U)$
51	50	impcom	$⊢ (φ \land (a \in B \land b \in B)) \to b \in U$
52	1 10 41 47 51 33 34	estrchom	$⊢ (φ \land (a \in B \land b \in B)) \to a Hom (E) b = {Base}_{b}^{{Base}_{a}}$
53	52	rexeqdv	$⊢ (φ \land (a \in B \land b \in B)) \to (\exists k \in (a Hom (E) b) h = (a G b) (k) \leftrightarrow \exists k \in ({Base}_{b}^{{Base}_{a}}) h = (a G b) (k))$
54	53	adantr	$⊢ ((φ \land (a \in B \land b \in B)) \land h : {Base}_{a} ⟶ {Base}_{b}) \to (\exists k \in (a Hom (E) b) h = (a G b) (k) \leftrightarrow \exists k \in ({Base}_{b}^{{Base}_{a}}) h = (a G b) (k))$
55	40 54	mpbird	$⊢ ((φ \land (a \in B \land b \in B)) \land h : {Base}_{a} ⟶ {Base}_{b}) \to \exists k \in (a Hom (E) b) h = (a G b) (k)$
56	55	ex	$⊢ (φ \land (a \in B \land b \in B)) \to (h : {Base}_{a} ⟶ {Base}_{b} \to \exists k \in (a Hom (E) b) h = (a G b) (k))$
57	22 56	sylbid	$⊢ (φ \land (a \in B \land b \in B)) \to (h \in (F (a) Hom (S) F (b)) \to \exists k \in (a Hom (E) b) h = (a G b) (k))$
58	57	ralrimiv	$⊢ (φ \land (a \in B \land b \in B)) \to \forall h \in (F (a) Hom (S) F (b)) \exists k \in (a Hom (E) b) h = (a G b) (k)$
59		dffo3	$⊢ (a G b) : a Hom (E) b \underset{onto}{⟶} F (a) Hom (S) F (b) \leftrightarrow ((a G b) : a Hom (E) b ⟶ F (a) Hom (S) F (b) \land \forall h \in (F (a) Hom (S) F (b)) \exists k \in (a Hom (E) b) h = (a G b) (k))$
60	9 58 59	sylanbrc	$⊢ (φ \land (a \in B \land b \in B)) \to (a G b) : a Hom (E) b \underset{onto}{⟶} F (a) Hom (S) F (b)$
61	60	ralrimivva	$⊢ φ \to \forall a \in B \forall b \in B (a G b) : a Hom (E) b \underset{onto}{⟶} F (a) Hom (S) F (b)$
62	3 11 41	isfull2	$⊢ F (E Full 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{onto}{⟶} F (a) Hom (S) F (b))$
63	8 61 62	sylanbrc	$⊢ φ \to F (E Full S) G$

Metamath Proof Explorer

Theorem fullestrcsetc

Proof