functhinclem4

Description: Lemma for functhinc . Other requirements on the morphism part are automatically satisfied. (Contributed by Zhi Wang, 1-Oct-2024)

	Ref	Expression
Hypotheses	functhinc.b	$⊢ B = {Base}_{D}$
	functhinc.c	$⊢ C = {Base}_{E}$
	functhinc.h	$⊢ H = Hom (D)$
	functhinc.j	$⊢ J = Hom (E)$
	functhinc.d	$⊢ φ \to D \in Cat$
	functhinc.e	No typesetting found for \|- ( ph -> E e. ThinCat ) with typecode \|-
	functhinc.f	$⊢ φ \to F : B ⟶ C$
	functhinc.k	$⊢ K = (x \in B, y \in B ⟼ (x H y) \times (F (x) J F (y)))$
	functhinc.1	$⊢ φ \to \forall z \in B \forall w \in B (F (z) J F (w) = \emptyset \to z H w = \emptyset)$
	functhinclem4.1	$⊢ \underset{˙}{1} = Id (D)$
	functhinclem4.i	$⊢ I = Id (E)$
	functhinclem4.x	$⊢ \underset{˙}{\cdot} = comp (D)$
	functhinclem4.o	$⊢ O = comp (E)$
Assertion	functhinclem4	$⊢ (φ \land G = K) \to \forall a \in B ((a G a) (\underset{˙}{1} (a)) = I (F (a)) \land \forall b \in B \forall c \in B \forall m \in (a H b) \forall n \in (b H c) (a G c) (n (⟨a, b⟩ \underset{˙}{\cdot} c) m) = (b G c) (n) (⟨F (a), F (b)⟩ O F (c)) (a G b) (m))$

Proof

Step	Hyp	Ref	Expression
1		functhinc.b	$⊢ B = {Base}_{D}$
2		functhinc.c	$⊢ C = {Base}_{E}$
3		functhinc.h	$⊢ H = Hom (D)$
4		functhinc.j	$⊢ J = Hom (E)$
5		functhinc.d	$⊢ φ \to D \in Cat$
6		functhinc.e	Could not format ( ph -> E e. ThinCat ) : No typesetting found for \|- ( ph -> E e. ThinCat ) with typecode \|-
7		functhinc.f	$⊢ φ \to F : B ⟶ C$
8		functhinc.k	$⊢ K = (x \in B, y \in B ⟼ (x H y) \times (F (x) J F (y)))$
9		functhinc.1	$⊢ φ \to \forall z \in B \forall w \in B (F (z) J F (w) = \emptyset \to z H w = \emptyset)$
10		functhinclem4.1	$⊢ \underset{˙}{1} = Id (D)$
11		functhinclem4.i	$⊢ I = Id (E)$
12		functhinclem4.x	$⊢ \underset{˙}{\cdot} = comp (D)$
13		functhinclem4.o	$⊢ O = comp (E)$
14	6	ad2antrr	Could not format ( ( ( ph /\ G = K ) /\ a e. B ) -> E e. ThinCat ) : No typesetting found for \|- ( ( ( ph /\ G = K ) /\ a e. B ) -> E e. ThinCat ) with typecode \|-
15	7	adantr	$⊢ (φ \land G = K) \to F : B ⟶ C$
16	15	ffvelcdmda	$⊢ ((φ \land G = K) \land a \in B) \to F (a) \in C$
17		simpr	$⊢ ((φ \land G = K) \land a \in B) \to a \in B$
18	5	ad2antrr	$⊢ ((φ \land G = K) \land a \in B) \to D \in Cat$
19	1 3 10 18 17	catidcl	$⊢ ((φ \land G = K) \land a \in B) \to \underset{˙}{1} (a) \in (a H a)$
20		simplr	$⊢ ((φ \land G = K) \land a \in B) \to G = K$
21		oveq1	$⊢ x = v \to x H y = v H y$
22		fveq2	$⊢ x = v \to F (x) = F (v)$
23	22	oveq1d	$⊢ x = v \to F (x) J F (y) = F (v) J F (y)$
24	21 23	xpeq12d	$⊢ x = v \to (x H y) \times (F (x) J F (y)) = (v H y) \times (F (v) J F (y))$
25		oveq2	$⊢ y = u \to v H y = v H u$
26		fveq2	$⊢ y = u \to F (y) = F (u)$
27	26	oveq2d	$⊢ y = u \to F (v) J F (y) = F (v) J F (u)$
28	25 27	xpeq12d	$⊢ y = u \to (v H y) \times (F (v) J F (y)) = (v H u) \times (F (v) J F (u))$
29	24 28	cbvmpov	$⊢ (x \in B, y \in B ⟼ (x H y) \times (F (x) J F (y))) = (v \in B, u \in B ⟼ (v H u) \times (F (v) J F (u)))$
30	8 29	eqtri	$⊢ K = (v \in B, u \in B ⟼ (v H u) \times (F (v) J F (u)))$
31	20 30	eqtrdi	$⊢ ((φ \land G = K) \land a \in B) \to G = (v \in B, u \in B ⟼ (v H u) \times (F (v) J F (u)))$
32	9	ad2antrr	$⊢ ((φ \land G = K) \land a \in B) \to \forall z \in B \forall w \in B (F (z) J F (w) = \emptyset \to z H w = \emptyset)$
33	17 17 32	functhinclem2	$⊢ ((φ \land G = K) \land a \in B) \to (F (a) J F (a) = \emptyset \to a H a = \emptyset)$
34	14 16 16 2 4	thincmo	$⊢ ((φ \land G = K) \land a \in B) \to \exists^{*} p p \in (F (a) J F (a))$
35	17 17 19 31 33 34	functhinclem3	$⊢ ((φ \land G = K) \land a \in B) \to (a G a) (\underset{˙}{1} (a)) \in (F (a) J F (a))$
36	14 2 4 16 11 35	thincid	$⊢ ((φ \land G = K) \land a \in B) \to (a G a) (\underset{˙}{1} (a)) = I (F (a))$
37	16	ad2antrr	$⊢ ((((φ \land G = K) \land a \in B) \land (b \in B \land c \in B)) \land (m \in (a H b) \land n \in (b H c))) \to F (a) \in C$
38	7	ad4antr	$⊢ ((((φ \land G = K) \land a \in B) \land (b \in B \land c \in B)) \land (m \in (a H b) \land n \in (b H c))) \to F : B ⟶ C$
39		simplrr	$⊢ ((((φ \land G = K) \land a \in B) \land (b \in B \land c \in B)) \land (m \in (a H b) \land n \in (b H c))) \to c \in B$
40	38 39	ffvelcdmd	$⊢ ((((φ \land G = K) \land a \in B) \land (b \in B \land c \in B)) \land (m \in (a H b) \land n \in (b H c))) \to F (c) \in C$
41	17	ad2antrr	$⊢ ((((φ \land G = K) \land a \in B) \land (b \in B \land c \in B)) \land (m \in (a H b) \land n \in (b H c))) \to a \in B$
42	5	ad4antr	$⊢ ((((φ \land G = K) \land a \in B) \land (b \in B \land c \in B)) \land (m \in (a H b) \land n \in (b H c))) \to D \in Cat$
43		simplrl	$⊢ ((((φ \land G = K) \land a \in B) \land (b \in B \land c \in B)) \land (m \in (a H b) \land n \in (b H c))) \to b \in B$
44		simprl	$⊢ ((((φ \land G = K) \land a \in B) \land (b \in B \land c \in B)) \land (m \in (a H b) \land n \in (b H c))) \to m \in (a H b)$
45		simprr	$⊢ ((((φ \land G = K) \land a \in B) \land (b \in B \land c \in B)) \land (m \in (a H b) \land n \in (b H c))) \to n \in (b H c)$
46	1 3 12 42 41 43 39 44 45	catcocl	$⊢ ((((φ \land G = K) \land a \in B) \land (b \in B \land c \in B)) \land (m \in (a H b) \land n \in (b H c))) \to n (⟨a, b⟩ \underset{˙}{\cdot} c) m \in (a H c)$
47	31	ad2antrr	$⊢ ((((φ \land G = K) \land a \in B) \land (b \in B \land c \in B)) \land (m \in (a H b) \land n \in (b H c))) \to G = (v \in B, u \in B ⟼ (v H u) \times (F (v) J F (u)))$
48	9	ad4antr	$⊢ ((((φ \land G = K) \land a \in B) \land (b \in B \land c \in B)) \land (m \in (a H b) \land n \in (b H c))) \to \forall z \in B \forall w \in B (F (z) J F (w) = \emptyset \to z H w = \emptyset)$
49	41 39 48	functhinclem2	$⊢ ((((φ \land G = K) \land a \in B) \land (b \in B \land c \in B)) \land (m \in (a H b) \land n \in (b H c))) \to (F (a) J F (c) = \emptyset \to a H c = \emptyset)$
50	6	ad4antr	Could not format ( ( ( ( ( ph /\ G = K ) /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ ( m e. ( a H b ) /\ n e. ( b H c ) ) ) -> E e. ThinCat ) : No typesetting found for \|- ( ( ( ( ( ph /\ G = K ) /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ ( m e. ( a H b ) /\ n e. ( b H c ) ) ) -> E e. ThinCat ) with typecode \|-
51	50 37 40 2 4	thincmo	$⊢ ((((φ \land G = K) \land a \in B) \land (b \in B \land c \in B)) \land (m \in (a H b) \land n \in (b H c))) \to \exists^{*} p p \in (F (a) J F (c))$
52	41 39 46 47 49 51	functhinclem3	$⊢ ((((φ \land G = K) \land a \in B) \land (b \in B \land c \in B)) \land (m \in (a H b) \land n \in (b H c))) \to (a G c) (n (⟨a, b⟩ \underset{˙}{\cdot} c) m) \in (F (a) J F (c))$
53	14	thinccd	$⊢ ((φ \land G = K) \land a \in B) \to E \in Cat$
54	53	ad2antrr	$⊢ ((((φ \land G = K) \land a \in B) \land (b \in B \land c \in B)) \land (m \in (a H b) \land n \in (b H c))) \to E \in Cat$
55	38 43	ffvelcdmd	$⊢ ((((φ \land G = K) \land a \in B) \land (b \in B \land c \in B)) \land (m \in (a H b) \land n \in (b H c))) \to F (b) \in C$
56	41 43 48	functhinclem2	$⊢ ((((φ \land G = K) \land a \in B) \land (b \in B \land c \in B)) \land (m \in (a H b) \land n \in (b H c))) \to (F (a) J F (b) = \emptyset \to a H b = \emptyset)$
57	50 37 55 2 4	thincmo	$⊢ ((((φ \land G = K) \land a \in B) \land (b \in B \land c \in B)) \land (m \in (a H b) \land n \in (b H c))) \to \exists^{*} p p \in (F (a) J F (b))$
58	41 43 44 47 56 57	functhinclem3	$⊢ ((((φ \land G = K) \land a \in B) \land (b \in B \land c \in B)) \land (m \in (a H b) \land n \in (b H c))) \to (a G b) (m) \in (F (a) J F (b))$
59	43 39 48	functhinclem2	$⊢ ((((φ \land G = K) \land a \in B) \land (b \in B \land c \in B)) \land (m \in (a H b) \land n \in (b H c))) \to (F (b) J F (c) = \emptyset \to b H c = \emptyset)$
60	50 55 40 2 4	thincmo	$⊢ ((((φ \land G = K) \land a \in B) \land (b \in B \land c \in B)) \land (m \in (a H b) \land n \in (b H c))) \to \exists^{*} p p \in (F (b) J F (c))$
61	43 39 45 47 59 60	functhinclem3	$⊢ ((((φ \land G = K) \land a \in B) \land (b \in B \land c \in B)) \land (m \in (a H b) \land n \in (b H c))) \to (b G c) (n) \in (F (b) J F (c))$
62	2 4 13 54 37 55 40 58 61	catcocl	$⊢ ((((φ \land G = K) \land a \in B) \land (b \in B \land c \in B)) \land (m \in (a H b) \land n \in (b H c))) \to (b G c) (n) (⟨F (a), F (b)⟩ O F (c)) (a G b) (m) \in (F (a) J F (c))$
63	37 40 52 62 2 4 50	thincmo2	$⊢ ((((φ \land G = K) \land a \in B) \land (b \in B \land c \in B)) \land (m \in (a H b) \land n \in (b H c))) \to (a G c) (n (⟨a, b⟩ \underset{˙}{\cdot} c) m) = (b G c) (n) (⟨F (a), F (b)⟩ O F (c)) (a G b) (m)$
64	63	ralrimivva	$⊢ (((φ \land G = K) \land a \in B) \land (b \in B \land c \in B)) \to \forall m \in (a H b) \forall n \in (b H c) (a G c) (n (⟨a, b⟩ \underset{˙}{\cdot} c) m) = (b G c) (n) (⟨F (a), F (b)⟩ O F (c)) (a G b) (m)$
65	64	ralrimivva	$⊢ ((φ \land G = K) \land a \in B) \to \forall b \in B \forall c \in B \forall m \in (a H b) \forall n \in (b H c) (a G c) (n (⟨a, b⟩ \underset{˙}{\cdot} c) m) = (b G c) (n) (⟨F (a), F (b)⟩ O F (c)) (a G b) (m)$
66	36 65	jca	$⊢ ((φ \land G = K) \land a \in B) \to ((a G a) (\underset{˙}{1} (a)) = I (F (a)) \land \forall b \in B \forall c \in B \forall m \in (a H b) \forall n \in (b H c) (a G c) (n (⟨a, b⟩ \underset{˙}{\cdot} c) m) = (b G c) (n) (⟨F (a), F (b)⟩ O F (c)) (a G b) (m))$
67	66	ralrimiva	$⊢ (φ \land G = K) \to \forall a \in B ((a G a) (\underset{˙}{1} (a)) = I (F (a)) \land \forall b \in B \forall c \in B \forall m \in (a H b) \forall n \in (b H c) (a G c) (n (⟨a, b⟩ \underset{˙}{\cdot} c) m) = (b G c) (n) (⟨F (a), F (b)⟩ O F (c)) (a G b) (m))$

Metamath Proof Explorer

Theorem functhinclem4

Proof