fullpropd

Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same full functors. (Contributed by Mario Carneiro, 27-Jan-2017)

	Ref	Expression
Hypotheses	fullpropd.1	$⊢ φ \to {Hom}_{𝑓} (A) = {Hom}_{𝑓} (B)$
	fullpropd.2	$⊢ φ \to {comp}_{𝑓} (A) = {comp}_{𝑓} (B)$
	fullpropd.3	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
	fullpropd.4	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
	fullpropd.a	$⊢ φ \to A \in V$
	fullpropd.b	$⊢ φ \to B \in V$
	fullpropd.c	$⊢ φ \to C \in V$
	fullpropd.d	$⊢ φ \to D \in V$
Assertion	fullpropd	$⊢ φ \to A Full C = B Full D$

Proof

Step	Hyp	Ref	Expression
1		fullpropd.1	$⊢ φ \to {Hom}_{𝑓} (A) = {Hom}_{𝑓} (B)$
2		fullpropd.2	$⊢ φ \to {comp}_{𝑓} (A) = {comp}_{𝑓} (B)$
3		fullpropd.3	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
4		fullpropd.4	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
5		fullpropd.a	$⊢ φ \to A \in V$
6		fullpropd.b	$⊢ φ \to B \in V$
7		fullpropd.c	$⊢ φ \to C \in V$
8		fullpropd.d	$⊢ φ \to D \in V$
9		relfull	$⊢ Rel (A Full C)$
10		relfull	$⊢ Rel (B Full D)$
11	1	homfeqbas	$⊢ φ \to {Base}_{A} = {Base}_{B}$
12	11	adantr	$⊢ (φ \land f (A Func C) g) \to {Base}_{A} = {Base}_{B}$
13	12	adantr	$⊢ ((φ \land f (A Func C) g) \land x \in {Base}_{A}) \to {Base}_{A} = {Base}_{B}$
14		eqid	$⊢ {Base}_{C} = {Base}_{C}$
15		eqid	$⊢ Hom (C) = Hom (C)$
16		eqid	$⊢ Hom (D) = Hom (D)$
17	3	ad3antrrr	$⊢ (((φ \land f (A Func C) g) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
18		eqid	$⊢ {Base}_{A} = {Base}_{A}$
19		simpllr	$⊢ (((φ \land f (A Func C) g) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \to f (A Func C) g$
20	18 14 19	funcf1	$⊢ (((φ \land f (A Func C) g) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \to f : {Base}_{A} ⟶ {Base}_{C}$
21		simplr	$⊢ (((φ \land f (A Func C) g) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \to x \in {Base}_{A}$
22	20 21	ffvelcdmd	$⊢ (((φ \land f (A Func C) g) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \to f (x) \in {Base}_{C}$
23		simpr	$⊢ (((φ \land f (A Func C) g) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \to y \in {Base}_{A}$
24	20 23	ffvelcdmd	$⊢ (((φ \land f (A Func C) g) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \to f (y) \in {Base}_{C}$
25	14 15 16 17 22 24	homfeqval	$⊢ (((φ \land f (A Func C) g) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \to f (x) Hom (C) f (y) = f (x) Hom (D) f (y)$
26	25	eqeq2d	$⊢ (((φ \land f (A Func C) g) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \to (ran (x g y) = f (x) Hom (C) f (y) \leftrightarrow ran (x g y) = f (x) Hom (D) f (y))$
27	13 26	raleqbidva	$⊢ ((φ \land f (A Func C) g) \land x \in {Base}_{A}) \to (\forall y \in {Base}_{A} ran (x g y) = f (x) Hom (C) f (y) \leftrightarrow \forall y \in {Base}_{B} ran (x g y) = f (x) Hom (D) f (y))$
28	12 27	raleqbidva	$⊢ (φ \land f (A Func C) g) \to (\forall x \in {Base}_{A} \forall y \in {Base}_{A} ran (x g y) = f (x) Hom (C) f (y) \leftrightarrow \forall x \in {Base}_{B} \forall y \in {Base}_{B} ran (x g y) = f (x) Hom (D) f (y))$
29	28	pm5.32da	$⊢ φ \to ((f (A Func C) g \land \forall x \in {Base}_{A} \forall y \in {Base}_{A} ran (x g y) = f (x) Hom (C) f (y)) \leftrightarrow (f (A Func C) g \land \forall x \in {Base}_{B} \forall y \in {Base}_{B} ran (x g y) = f (x) Hom (D) f (y)))$
30	1 2 3 4 5 6 7 8	funcpropd	$⊢ φ \to A Func C = B Func D$
31	30	breqd	$⊢ φ \to (f (A Func C) g \leftrightarrow f (B Func D) g)$
32	31	anbi1d	$⊢ φ \to ((f (A Func C) g \land \forall x \in {Base}_{B} \forall y \in {Base}_{B} ran (x g y) = f (x) Hom (D) f (y)) \leftrightarrow (f (B Func D) g \land \forall x \in {Base}_{B} \forall y \in {Base}_{B} ran (x g y) = f (x) Hom (D) f (y)))$
33	29 32	bitrd	$⊢ φ \to ((f (A Func C) g \land \forall x \in {Base}_{A} \forall y \in {Base}_{A} ran (x g y) = f (x) Hom (C) f (y)) \leftrightarrow (f (B Func D) g \land \forall x \in {Base}_{B} \forall y \in {Base}_{B} ran (x g y) = f (x) Hom (D) f (y)))$
34	18 15	isfull	$⊢ f (A Full C) g \leftrightarrow (f (A Func C) g \land \forall x \in {Base}_{A} \forall y \in {Base}_{A} ran (x g y) = f (x) Hom (C) f (y))$
35		eqid	$⊢ {Base}_{B} = {Base}_{B}$
36	35 16	isfull	$⊢ f (B Full D) g \leftrightarrow (f (B Func D) g \land \forall x \in {Base}_{B} \forall y \in {Base}_{B} ran (x g y) = f (x) Hom (D) f (y))$
37	33 34 36	3bitr4g	$⊢ φ \to (f (A Full C) g \leftrightarrow f (B Full D) g)$
38	9 10 37	eqbrrdiv	$⊢ φ \to A Full C = B Full D$

Metamath Proof Explorer

Theorem fullpropd

Proof