Theorem functhinclem4 49728

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

Hypotheses

Ref	Expression
functhinc.b	⊢ 𝐵 = (Base‘𝐷)
functhinc.c	⊢ 𝐶 = (Base‘𝐸)
functhinc.h	⊢ 𝐻 = (Hom ‘𝐷)
functhinc.j	⊢ 𝐽 = (Hom ‘𝐸)
functhinc.d	⊢ (𝜑 → 𝐷 ∈ Cat)
functhinc.e	⊢ (𝜑 → 𝐸 ∈ ThinCat)
functhinc.f	⊢ (𝜑 → 𝐹:𝐵⟶𝐶)
functhinc.k	⊢ 𝐾 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))))
functhinc.1	⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅))
functhinclem4.1	⊢ 1 = (Id‘𝐷)
functhinclem4.i	⊢ 𝐼 = (Id‘𝐸)
functhinclem4.x	⊢ · = (comp‘𝐷)
functhinclem4.o	⊢ 𝑂 = (comp‘𝐸)

Assertion

Ref	Expression
functhinclem4	⊢ ((𝜑 ∧ 𝐺 = 𝐾) → ∀𝑎 ∈ 𝐵 (((𝑎𝐺𝑎)‘( 1 ‘𝑎)) = (𝐼‘(𝐹‘𝑎)) ∧ ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑚 ∈ (𝑎𝐻𝑏)∀𝑛 ∈ (𝑏𝐻𝑐)((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) = (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚))))

Distinct variable groups:   𝐵,𝑏,𝑐,𝑚,𝑛   𝑤,𝐵,𝑧,𝑏,𝑐   𝑥,𝐵,𝑦   𝑥,𝐹,𝑦   𝑤,𝐹,𝑧   𝐺,𝑎,𝑏,𝑐,𝑚,𝑛   𝑛,𝐻   𝑤,𝐻,𝑧   𝑥,𝐻,𝑦   𝑥,𝐽,𝑦   𝑤,𝐽,𝑧   𝐾,𝑎,𝑏,𝑐,𝑚,𝑛   𝜑,𝑎,𝑏,𝑐,𝑚,𝑛   𝑤,𝑎,𝑧

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑤)   𝐵(𝑎)   𝐶(𝑥,𝑦,𝑧,𝑤,𝑚,𝑛,𝑎,𝑏,𝑐)   𝐷(𝑥,𝑦,𝑧,𝑤,𝑚,𝑛,𝑎,𝑏,𝑐)   · (𝑥,𝑦,𝑧,𝑤,𝑚,𝑛,𝑎,𝑏,𝑐)   1 (𝑥,𝑦,𝑧,𝑤,𝑚,𝑛,𝑎,𝑏,𝑐)   𝐸(𝑥,𝑦,𝑧,𝑤,𝑚,𝑛,𝑎,𝑏,𝑐)   𝐹(𝑚,𝑛,𝑎,𝑏,𝑐)   𝐺(𝑥,𝑦,𝑧,𝑤)   𝐻(𝑚,𝑎,𝑏,𝑐)   𝐼(𝑥,𝑦,𝑧,𝑤,𝑚,𝑛,𝑎,𝑏,𝑐)   𝐽(𝑚,𝑛,𝑎,𝑏,𝑐)   𝐾(𝑥,𝑦,𝑧,𝑤)   𝑂(𝑥,𝑦,𝑧,𝑤,𝑚,𝑛,𝑎,𝑏,𝑐)

Proof of Theorem functhinclem4

Dummy variables 𝑝 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		functhinc.e	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ ThinCat)
2	1	ad2antrr 727	. . . 4 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → 𝐸 ∈ ThinCat)
3		functhinc.c	. . . 4 ⊢ 𝐶 = (Base‘𝐸)
4		functhinc.j	. . . 4 ⊢ 𝐽 = (Hom ‘𝐸)
5		functhinc.f	. . . . . 6 ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)
6	5	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝐺 = 𝐾) → 𝐹:𝐵⟶𝐶)
7	6	ffvelcdmda 7031	. . . 4 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → (𝐹‘𝑎) ∈ 𝐶)
8		functhinclem4.i	. . . 4 ⊢ 𝐼 = (Id‘𝐸)
9		simpr 484	. . . . 5 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → 𝑎 ∈ 𝐵)
10		functhinc.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐷)
11		functhinc.h	. . . . . 6 ⊢ 𝐻 = (Hom ‘𝐷)
12		functhinclem4.1	. . . . . 6 ⊢ 1 = (Id‘𝐷)
13		functhinc.d	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ Cat)
14	13	ad2antrr 727	. . . . . 6 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → 𝐷 ∈ Cat)
15	10, 11, 12, 14, 9	catidcl 17609	. . . . 5 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → ( 1 ‘𝑎) ∈ (𝑎𝐻𝑎))
16		simplr 769	. . . . . 6 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → 𝐺 = 𝐾)
17		functhinc.k	. . . . . . 7 ⊢ 𝐾 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))))
18		oveq1 7367	. . . . . . . . 9 ⊢ (𝑥 = 𝑣 → (𝑥𝐻𝑦) = (𝑣𝐻𝑦))
19		fveq2 6835	. . . . . . . . . 10 ⊢ (𝑥 = 𝑣 → (𝐹‘𝑥) = (𝐹‘𝑣))
20	19	oveq1d 7375	. . . . . . . . 9 ⊢ (𝑥 = 𝑣 → ((𝐹‘𝑥)𝐽(𝐹‘𝑦)) = ((𝐹‘𝑣)𝐽(𝐹‘𝑦)))
21	18, 20	xpeq12d 5656	. . . . . . . 8 ⊢ (𝑥 = 𝑣 → ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))) = ((𝑣𝐻𝑦) × ((𝐹‘𝑣)𝐽(𝐹‘𝑦))))
22		oveq2 7368	. . . . . . . . 9 ⊢ (𝑦 = 𝑢 → (𝑣𝐻𝑦) = (𝑣𝐻𝑢))
23		fveq2 6835	. . . . . . . . . 10 ⊢ (𝑦 = 𝑢 → (𝐹‘𝑦) = (𝐹‘𝑢))
24	23	oveq2d 7376	. . . . . . . . 9 ⊢ (𝑦 = 𝑢 → ((𝐹‘𝑣)𝐽(𝐹‘𝑦)) = ((𝐹‘𝑣)𝐽(𝐹‘𝑢)))
25	22, 24	xpeq12d 5656	. . . . . . . 8 ⊢ (𝑦 = 𝑢 → ((𝑣𝐻𝑦) × ((𝐹‘𝑣)𝐽(𝐹‘𝑦))) = ((𝑣𝐻𝑢) × ((𝐹‘𝑣)𝐽(𝐹‘𝑢))))
26	21, 25	cbvmpov 7455	. . . . . . 7 ⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) = (𝑣 ∈ 𝐵, 𝑢 ∈ 𝐵 ↦ ((𝑣𝐻𝑢) × ((𝐹‘𝑣)𝐽(𝐹‘𝑢))))
27	17, 26	eqtri 2760	. . . . . 6 ⊢ 𝐾 = (𝑣 ∈ 𝐵, 𝑢 ∈ 𝐵 ↦ ((𝑣𝐻𝑢) × ((𝐹‘𝑣)𝐽(𝐹‘𝑢))))
28	16, 27	eqtrdi 2788	. . . . 5 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → 𝐺 = (𝑣 ∈ 𝐵, 𝑢 ∈ 𝐵 ↦ ((𝑣𝐻𝑢) × ((𝐹‘𝑣)𝐽(𝐹‘𝑢)))))
29		functhinc.1	. . . . . . 7 ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅))
30	29	ad2antrr 727	. . . . . 6 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅))
31	9, 9, 30	functhinclem2 49726	. . . . 5 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → (((𝐹‘𝑎)𝐽(𝐹‘𝑎)) = ∅ → (𝑎𝐻𝑎) = ∅))
32	2, 7, 7, 3, 4	thincmo 49709	. . . . 5 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → ∃*𝑝 𝑝 ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑎)))
33	9, 9, 15, 28, 31, 32	functhinclem3 49727	. . . 4 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → ((𝑎𝐺𝑎)‘( 1 ‘𝑎)) ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑎)))
34	2, 3, 4, 7, 8, 33	thincid 49713	. . 3 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → ((𝑎𝐺𝑎)‘( 1 ‘𝑎)) = (𝐼‘(𝐹‘𝑎)))
35	7	ad2antrr 727	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (𝐹‘𝑎) ∈ 𝐶)
36	5	ad4antr 733	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝐹:𝐵⟶𝐶)
37		simplrr 778	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝑐 ∈ 𝐵)
38	36, 37	ffvelcdmd 7032	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (𝐹‘𝑐) ∈ 𝐶)
39	9	ad2antrr 727	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝑎 ∈ 𝐵)
40		functhinclem4.x	. . . . . . . 8 ⊢ · = (comp‘𝐷)
41	13	ad4antr 733	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝐷 ∈ Cat)
42		simplrl 777	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝑏 ∈ 𝐵)
43		simprl 771	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝑚 ∈ (𝑎𝐻𝑏))
44		simprr 773	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝑛 ∈ (𝑏𝐻𝑐))
45	10, 11, 40, 41, 39, 42, 37, 43, 44	catcocl 17612	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚) ∈ (𝑎𝐻𝑐))
46	28	ad2antrr 727	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝐺 = (𝑣 ∈ 𝐵, 𝑢 ∈ 𝐵 ↦ ((𝑣𝐻𝑢) × ((𝐹‘𝑣)𝐽(𝐹‘𝑢)))))
47	29	ad4antr 733	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅))
48	39, 37, 47	functhinclem2 49726	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (((𝐹‘𝑎)𝐽(𝐹‘𝑐)) = ∅ → (𝑎𝐻𝑐) = ∅))
49	1	ad4antr 733	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝐸 ∈ ThinCat)
50	49, 35, 38, 3, 4	thincmo 49709	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ∃*𝑝 𝑝 ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑐)))
51	39, 37, 45, 46, 48, 50	functhinclem3 49727	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑐)))
52		functhinclem4.o	. . . . . . 7 ⊢ 𝑂 = (comp‘𝐸)
53	2	thinccd 49704	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → 𝐸 ∈ Cat)
54	53	ad2antrr 727	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝐸 ∈ Cat)
55	36, 42	ffvelcdmd 7032	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (𝐹‘𝑏) ∈ 𝐶)
56	39, 42, 47	functhinclem2 49726	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (((𝐹‘𝑎)𝐽(𝐹‘𝑏)) = ∅ → (𝑎𝐻𝑏) = ∅))
57	49, 35, 55, 3, 4	thincmo 49709	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ∃*𝑝 𝑝 ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑏)))
58	39, 42, 43, 46, 56, 57	functhinclem3 49727	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ((𝑎𝐺𝑏)‘𝑚) ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑏)))
59	42, 37, 47	functhinclem2 49726	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (((𝐹‘𝑏)𝐽(𝐹‘𝑐)) = ∅ → (𝑏𝐻𝑐) = ∅))
60	49, 55, 38, 3, 4	thincmo 49709	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ∃*𝑝 𝑝 ∈ ((𝐹‘𝑏)𝐽(𝐹‘𝑐)))
61	42, 37, 44, 46, 59, 60	functhinclem3 49727	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ((𝑏𝐺𝑐)‘𝑛) ∈ ((𝐹‘𝑏)𝐽(𝐹‘𝑐)))
62	3, 4, 52, 54, 35, 55, 38, 58, 61	catcocl 17612	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚)) ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑐)))
63	35, 38, 51, 62, 3, 4, 49	thincmo2 49707	. . . . 5 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) = (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚)))
64	63	ralrimivva 3180	. . . 4 ⊢ ((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → ∀𝑚 ∈ (𝑎𝐻𝑏)∀𝑛 ∈ (𝑏𝐻𝑐)((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) = (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚)))
65	64	ralrimivva 3180	. . 3 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑚 ∈ (𝑎𝐻𝑏)∀𝑛 ∈ (𝑏𝐻𝑐)((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) = (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚)))
66	34, 65	jca 511	. 2 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → (((𝑎𝐺𝑎)‘( 1 ‘𝑎)) = (𝐼‘(𝐹‘𝑎)) ∧ ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑚 ∈ (𝑎𝐻𝑏)∀𝑛 ∈ (𝑏𝐻𝑐)((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) = (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚))))
67	66	ralrimiva 3129	1 ⊢ ((𝜑 ∧ 𝐺 = 𝐾) → ∀𝑎 ∈ 𝐵 (((𝑎𝐺𝑎)‘( 1 ‘𝑎)) = (𝐼‘(𝐹‘𝑎)) ∧ ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑚 ∈ (𝑎𝐻𝑏)∀𝑛 ∈ (𝑏𝐻𝑐)((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) = (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚))))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ∅c0 4286  ⟨cop 4587   × cxp 5623  ⟶wf 6489  ‘cfv 6493  (class class class)co 7360   ∈ cmpo 7362  Basecbs 17140  Hom chom 17192  compcco 17193  Catccat 17591  Idccid 17592  ThinCatcthinc 49698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5225  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rmo 3351  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-iun 4949  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-cat 17595  df-cid 17596  df-thinc 49699

This theorem is referenced by:  functhinc  49729