Theorem functhinclem4 46277

Description: Lemma for functhinc 46278. 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 722	. . . 4 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → 𝐸 ∈ ThinCat)
3		functhinc.c	. . . 4 ⊢ 𝐶 = (Base‘𝐸)
4		functhinc.j	. . . 4 ⊢ 𝐽 = (Hom ‘𝐸)
5		functhinc.f	. . . . . 6 ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)
6	5	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝐺 = 𝐾) → 𝐹:𝐵⟶𝐶)
7	6	ffvelrnda 6955	. . . 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 722	. . . . . 6 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → 𝐷 ∈ Cat)
15	10, 11, 12, 14, 9	catidcl 17372	. . . . 5 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → ( 1 ‘𝑎) ∈ (𝑎𝐻𝑎))
16		simplr 765	. . . . . 6 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → 𝐺 = 𝐾)
17		functhinc.k	. . . . . . 7 ⊢ 𝐾 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))))
18		oveq1 7275	. . . . . . . . 9 ⊢ (𝑥 = 𝑣 → (𝑥𝐻𝑦) = (𝑣𝐻𝑦))
19		fveq2 6768	. . . . . . . . . 10 ⊢ (𝑥 = 𝑣 → (𝐹‘𝑥) = (𝐹‘𝑣))
20	19	oveq1d 7283	. . . . . . . . 9 ⊢ (𝑥 = 𝑣 → ((𝐹‘𝑥)𝐽(𝐹‘𝑦)) = ((𝐹‘𝑣)𝐽(𝐹‘𝑦)))
21	18, 20	xpeq12d 5619	. . . . . . . 8 ⊢ (𝑥 = 𝑣 → ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))) = ((𝑣𝐻𝑦) × ((𝐹‘𝑣)𝐽(𝐹‘𝑦))))
22		oveq2 7276	. . . . . . . . 9 ⊢ (𝑦 = 𝑢 → (𝑣𝐻𝑦) = (𝑣𝐻𝑢))
23		fveq2 6768	. . . . . . . . . 10 ⊢ (𝑦 = 𝑢 → (𝐹‘𝑦) = (𝐹‘𝑢))
24	23	oveq2d 7284	. . . . . . . . 9 ⊢ (𝑦 = 𝑢 → ((𝐹‘𝑣)𝐽(𝐹‘𝑦)) = ((𝐹‘𝑣)𝐽(𝐹‘𝑢)))
25	22, 24	xpeq12d 5619	. . . . . . . 8 ⊢ (𝑦 = 𝑢 → ((𝑣𝐻𝑦) × ((𝐹‘𝑣)𝐽(𝐹‘𝑦))) = ((𝑣𝐻𝑢) × ((𝐹‘𝑣)𝐽(𝐹‘𝑢))))
26	21, 25	cbvmpov 7361	. . . . . . 7 ⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) = (𝑣 ∈ 𝐵, 𝑢 ∈ 𝐵 ↦ ((𝑣𝐻𝑢) × ((𝐹‘𝑣)𝐽(𝐹‘𝑢))))
27	17, 26	eqtri 2767	. . . . . 6 ⊢ 𝐾 = (𝑣 ∈ 𝐵, 𝑢 ∈ 𝐵 ↦ ((𝑣𝐻𝑢) × ((𝐹‘𝑣)𝐽(𝐹‘𝑢))))
28	16, 27	eqtrdi 2795	. . . . 5 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → 𝐺 = (𝑣 ∈ 𝐵, 𝑢 ∈ 𝐵 ↦ ((𝑣𝐻𝑢) × ((𝐹‘𝑣)𝐽(𝐹‘𝑢)))))
29		functhinc.1	. . . . . . 7 ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅))
30	29	ad2antrr 722	. . . . . 6 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅))
31	9, 9, 30	functhinclem2 46275	. . . . 5 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → (((𝐹‘𝑎)𝐽(𝐹‘𝑎)) = ∅ → (𝑎𝐻𝑎) = ∅))
32	2, 7, 7, 3, 4	thincmo 46262	. . . . 5 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → ∃*𝑝 𝑝 ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑎)))
33	9, 9, 15, 28, 31, 32	functhinclem3 46276	. . . 4 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → ((𝑎𝐺𝑎)‘( 1 ‘𝑎)) ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑎)))
34	2, 3, 4, 7, 8, 33	thincid 46266	. . 3 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → ((𝑎𝐺𝑎)‘( 1 ‘𝑎)) = (𝐼‘(𝐹‘𝑎)))
35	7	ad2antrr 722	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (𝐹‘𝑎) ∈ 𝐶)
36	5	ad4antr 728	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝐹:𝐵⟶𝐶)
37		simplrr 774	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝑐 ∈ 𝐵)
38	36, 37	ffvelrnd 6956	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (𝐹‘𝑐) ∈ 𝐶)
39	9	ad2antrr 722	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝑎 ∈ 𝐵)
40		functhinclem4.x	. . . . . . . 8 ⊢ · = (comp‘𝐷)
41	13	ad4antr 728	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝐷 ∈ Cat)
42		simplrl 773	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝑏 ∈ 𝐵)
43		simprl 767	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝑚 ∈ (𝑎𝐻𝑏))
44		simprr 769	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝑛 ∈ (𝑏𝐻𝑐))
45	10, 11, 40, 41, 39, 42, 37, 43, 44	catcocl 17375	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚) ∈ (𝑎𝐻𝑐))
46	28	ad2antrr 722	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝐺 = (𝑣 ∈ 𝐵, 𝑢 ∈ 𝐵 ↦ ((𝑣𝐻𝑢) × ((𝐹‘𝑣)𝐽(𝐹‘𝑢)))))
47	29	ad4antr 728	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅))
48	39, 37, 47	functhinclem2 46275	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (((𝐹‘𝑎)𝐽(𝐹‘𝑐)) = ∅ → (𝑎𝐻𝑐) = ∅))
49	1	ad4antr 728	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝐸 ∈ ThinCat)
50	49, 35, 38, 3, 4	thincmo 46262	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ∃*𝑝 𝑝 ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑐)))
51	39, 37, 45, 46, 48, 50	functhinclem3 46276	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑐)))
52		functhinclem4.o	. . . . . . 7 ⊢ 𝑂 = (comp‘𝐸)
53	2	thinccd 46258	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → 𝐸 ∈ Cat)
54	53	ad2antrr 722	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝐸 ∈ Cat)
55	36, 42	ffvelrnd 6956	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (𝐹‘𝑏) ∈ 𝐶)
56	39, 42, 47	functhinclem2 46275	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (((𝐹‘𝑎)𝐽(𝐹‘𝑏)) = ∅ → (𝑎𝐻𝑏) = ∅))
57	49, 35, 55, 3, 4	thincmo 46262	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ∃*𝑝 𝑝 ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑏)))
58	39, 42, 43, 46, 56, 57	functhinclem3 46276	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ((𝑎𝐺𝑏)‘𝑚) ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑏)))
59	42, 37, 47	functhinclem2 46275	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (((𝐹‘𝑏)𝐽(𝐹‘𝑐)) = ∅ → (𝑏𝐻𝑐) = ∅))
60	49, 55, 38, 3, 4	thincmo 46262	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ∃*𝑝 𝑝 ∈ ((𝐹‘𝑏)𝐽(𝐹‘𝑐)))
61	42, 37, 44, 46, 59, 60	functhinclem3 46276	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ((𝑏𝐺𝑐)‘𝑛) ∈ ((𝐹‘𝑏)𝐽(𝐹‘𝑐)))
62	3, 4, 52, 54, 35, 55, 38, 58, 61	catcocl 17375	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚)) ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑐)))
63	35, 38, 51, 62, 3, 4, 49	thincmo2 46261	. . . . 5 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) = (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚)))
64	63	ralrimivva 3116	. . . 4 ⊢ ((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → ∀𝑚 ∈ (𝑎𝐻𝑏)∀𝑛 ∈ (𝑏𝐻𝑐)((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) = (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚)))
65	64	ralrimivva 3116	. . 3 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑚 ∈ (𝑎𝐻𝑏)∀𝑛 ∈ (𝑏𝐻𝑐)((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) = (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚)))
66	34, 65	jca 511	. 2 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → (((𝑎𝐺𝑎)‘( 1 ‘𝑎)) = (𝐼‘(𝐹‘𝑎)) ∧ ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑚 ∈ (𝑎𝐻𝑏)∀𝑛 ∈ (𝑏𝐻𝑐)((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) = (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚))))
67	66	ralrimiva 3109	1 ⊢ ((𝜑 ∧ 𝐺 = 𝐾) → ∀𝑎 ∈ 𝐵 (((𝑎𝐺𝑎)‘( 1 ‘𝑎)) = (𝐼‘(𝐹‘𝑎)) ∧ ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑚 ∈ (𝑎𝐻𝑏)∀𝑛 ∈ (𝑏𝐻𝑐)((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) = (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚))))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2109  ∀wral 3065  ∅c0 4261  ⟨cop 4572   × cxp 5586  ⟶wf 6426  ‘cfv 6430  (class class class)co 7268   ∈ cmpo 7270  Basecbs 16893  Hom chom 16954  compcco 16955  Catccat 17354  Idccid 17355  ThinCatcthinc 46252

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-rep 5213  ax-sep 5226  ax-nul 5233  ax-pow 5291  ax-pr 5355  ax-un 7579

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3072  df-rmo 3073  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-iun 4931  df-br 5079  df-opab 5141  df-mpt 5162  df-id 5488  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-f1 6435  df-fo 6436  df-f1o 6437  df-fv 6438  df-riota 7225  df-ov 7271  df-oprab 7272  df-mpo 7273  df-cat 17358  df-cid 17359  df-thinc 46253

This theorem is referenced by:  functhinc  46278