Theorem functhinclem4 50069

Description: Lemma for functhinc 50070. 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 736	. . . 4 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → 𝐸 ∈ ThinCat)
3		functhinc.c	. . . 4 ⊢ 𝐶 = (Base‘𝐸)
4		functhinc.j	. . . 4 ⊢ 𝐽 = (Hom ‘𝐸)
5		functhinc.f	. . . . . 6 ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)
6	5	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝐺 = 𝐾) → 𝐹:𝐵⟶𝐶)
7	6	ffvelcdmda 7066	. . . 4 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → (𝐹‘𝑎) ∈ 𝐶)
8		functhinclem4.i	. . . 4 ⊢ 𝐼 = (Id‘𝐸)
9		simpr 488	. . . . 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 736	. . . . . 6 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → 𝐷 ∈ Cat)
15	10, 11, 12, 14, 9	catidcl 17715	. . . . 5 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → ( 1 ‘𝑎) ∈ (𝑎𝐻𝑎))
16		simplr 778	. . . . . 6 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → 𝐺 = 𝐾)
17		functhinc.k	. . . . . . 7 ⊢ 𝐾 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))))
18		oveq1 7404	. . . . . . . . 9 ⊢ (𝑥 = 𝑣 → (𝑥𝐻𝑦) = (𝑣𝐻𝑦))
19		fveq2 6868	. . . . . . . . . 10 ⊢ (𝑥 = 𝑣 → (𝐹‘𝑥) = (𝐹‘𝑣))
20	19	oveq1d 7412	. . . . . . . . 9 ⊢ (𝑥 = 𝑣 → ((𝐹‘𝑥)𝐽(𝐹‘𝑦)) = ((𝐹‘𝑣)𝐽(𝐹‘𝑦)))
21	18, 20	xpeq12d 5679	. . . . . . . 8 ⊢ (𝑥 = 𝑣 → ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))) = ((𝑣𝐻𝑦) × ((𝐹‘𝑣)𝐽(𝐹‘𝑦))))
22		oveq2 7405	. . . . . . . . 9 ⊢ (𝑦 = 𝑢 → (𝑣𝐻𝑦) = (𝑣𝐻𝑢))
23		fveq2 6868	. . . . . . . . . 10 ⊢ (𝑦 = 𝑢 → (𝐹‘𝑦) = (𝐹‘𝑢))
24	23	oveq2d 7413	. . . . . . . . 9 ⊢ (𝑦 = 𝑢 → ((𝐹‘𝑣)𝐽(𝐹‘𝑦)) = ((𝐹‘𝑣)𝐽(𝐹‘𝑢)))
25	22, 24	xpeq12d 5679	. . . . . . . 8 ⊢ (𝑦 = 𝑢 → ((𝑣𝐻𝑦) × ((𝐹‘𝑣)𝐽(𝐹‘𝑦))) = ((𝑣𝐻𝑢) × ((𝐹‘𝑣)𝐽(𝐹‘𝑢))))
26	21, 25	cbvmpov 7492	. . . . . . 7 ⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) = (𝑣 ∈ 𝐵, 𝑢 ∈ 𝐵 ↦ ((𝑣𝐻𝑢) × ((𝐹‘𝑣)𝐽(𝐹‘𝑢))))
27	17, 26	eqtri 2786	. . . . . 6 ⊢ 𝐾 = (𝑣 ∈ 𝐵, 𝑢 ∈ 𝐵 ↦ ((𝑣𝐻𝑢) × ((𝐹‘𝑣)𝐽(𝐹‘𝑢))))
28	16, 27	eqtrdi 2814	. . . . 5 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → 𝐺 = (𝑣 ∈ 𝐵, 𝑢 ∈ 𝐵 ↦ ((𝑣𝐻𝑢) × ((𝐹‘𝑣)𝐽(𝐹‘𝑢)))))
29		functhinc.1	. . . . . . 7 ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅))
30	29	ad2antrr 736	. . . . . 6 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅))
31	9, 9, 30	functhinclem2 50067	. . . . 5 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → (((𝐹‘𝑎)𝐽(𝐹‘𝑎)) = ∅ → (𝑎𝐻𝑎) = ∅))
32	2, 7, 7, 3, 4	thincmo 50050	. . . . 5 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → ∃*𝑝 𝑝 ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑎)))
33	9, 9, 15, 28, 31, 32	functhinclem3 50068	. . . 4 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → ((𝑎𝐺𝑎)‘( 1 ‘𝑎)) ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑎)))
34	2, 3, 4, 7, 8, 33	thincid 50054	. . 3 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → ((𝑎𝐺𝑎)‘( 1 ‘𝑎)) = (𝐼‘(𝐹‘𝑎)))
35	7	ad2antrr 736	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (𝐹‘𝑎) ∈ 𝐶)
36	5	ad4antr 742	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝐹:𝐵⟶𝐶)
37		simplrr 787	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝑐 ∈ 𝐵)
38	36, 37	ffvelcdmd 7067	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (𝐹‘𝑐) ∈ 𝐶)
39	9	ad2antrr 736	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝑎 ∈ 𝐵)
40		functhinclem4.x	. . . . . . . 8 ⊢ · = (comp‘𝐷)
41	13	ad4antr 742	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝐷 ∈ Cat)
42		simplrl 786	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝑏 ∈ 𝐵)
43		simprl 780	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝑚 ∈ (𝑎𝐻𝑏))
44		simprr 782	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝑛 ∈ (𝑏𝐻𝑐))
45	10, 11, 40, 41, 39, 42, 37, 43, 44	catcocl 17718	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚) ∈ (𝑎𝐻𝑐))
46	28	ad2antrr 736	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝐺 = (𝑣 ∈ 𝐵, 𝑢 ∈ 𝐵 ↦ ((𝑣𝐻𝑢) × ((𝐹‘𝑣)𝐽(𝐹‘𝑢)))))
47	29	ad4antr 742	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅))
48	39, 37, 47	functhinclem2 50067	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (((𝐹‘𝑎)𝐽(𝐹‘𝑐)) = ∅ → (𝑎𝐻𝑐) = ∅))
49	1	ad4antr 742	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝐸 ∈ ThinCat)
50	49, 35, 38, 3, 4	thincmo 50050	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ∃*𝑝 𝑝 ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑐)))
51	39, 37, 45, 46, 48, 50	functhinclem3 50068	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑐)))
52		functhinclem4.o	. . . . . . 7 ⊢ 𝑂 = (comp‘𝐸)
53	2	thinccd 50045	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → 𝐸 ∈ Cat)
54	53	ad2antrr 736	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝐸 ∈ Cat)
55	36, 42	ffvelcdmd 7067	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (𝐹‘𝑏) ∈ 𝐶)
56	39, 42, 47	functhinclem2 50067	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (((𝐹‘𝑎)𝐽(𝐹‘𝑏)) = ∅ → (𝑎𝐻𝑏) = ∅))
57	49, 35, 55, 3, 4	thincmo 50050	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ∃*𝑝 𝑝 ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑏)))
58	39, 42, 43, 46, 56, 57	functhinclem3 50068	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ((𝑎𝐺𝑏)‘𝑚) ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑏)))
59	42, 37, 47	functhinclem2 50067	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (((𝐹‘𝑏)𝐽(𝐹‘𝑐)) = ∅ → (𝑏𝐻𝑐) = ∅))
60	49, 55, 38, 3, 4	thincmo 50050	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ∃*𝑝 𝑝 ∈ ((𝐹‘𝑏)𝐽(𝐹‘𝑐)))
61	42, 37, 44, 46, 59, 60	functhinclem3 50068	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ((𝑏𝐺𝑐)‘𝑛) ∈ ((𝐹‘𝑏)𝐽(𝐹‘𝑐)))
62	3, 4, 52, 54, 35, 55, 38, 58, 61	catcocl 17718	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚)) ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑐)))
63	35, 38, 51, 62, 3, 4, 49	thincmo2 50048	. . . . 5 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) = (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚)))
64	63	ralrimivva 3206	. . . 4 ⊢ ((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → ∀𝑚 ∈ (𝑎𝐻𝑏)∀𝑛 ∈ (𝑏𝐻𝑐)((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) = (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚)))
65	64	ralrimivva 3206	. . 3 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑚 ∈ (𝑎𝐻𝑏)∀𝑛 ∈ (𝑏𝐻𝑐)((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) = (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚)))
66	34, 65	jca 519	. 2 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → (((𝑎𝐺𝑎)‘( 1 ‘𝑎)) = (𝐼‘(𝐹‘𝑎)) ∧ ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑚 ∈ (𝑎𝐻𝑏)∀𝑛 ∈ (𝑏𝐻𝑐)((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) = (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚))))
67	66	ralrimiva 3155	1 ⊢ ((𝜑 ∧ 𝐺 = 𝐾) → ∀𝑎 ∈ 𝐵 (((𝑎𝐺𝑎)‘( 1 ‘𝑎)) = (𝐼‘(𝐹‘𝑎)) ∧ ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑚 ∈ (𝑎𝐻𝑏)∀𝑛 ∈ (𝑏𝐻𝑐)((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) = (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚))))

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1561   ∈ wcel 2143  ∀wral 3077  ∅c0 4286  ⟨cop 4589   × cxp 5646  ⟶wf 6518  ‘cfv 6522  (class class class)co 7397   ∈ cmpo 7399  Basecbs 17246  Hom chom 17298  compcco 17299  Catccat 17697  Idccid 17698  ThinCatcthinc 50039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5228  ax-sep 5247  ax-nul 5257  ax-pow 5323  ax-pr 5391  ax-un 7719

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3078  df-rex 3088  df-rmo 3368  df-reu 3369  df-rab 3416  df-v 3457  df-sbc 3746  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5102  df-opab 5164  df-mpt 5183  df-id 5543  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-iota 6478  df-fun 6524  df-fn 6525  df-f 6526  df-f1 6527  df-fo 6528  df-f1o 6529  df-fv 6530  df-riota 7354  df-ov 7400  df-oprab 7401  df-mpo 7402  df-cat 17701  df-cid 17702  df-thinc 50040

This theorem is referenced by:  functhinc  50070