Theorem functhinclem4 48711

Description: Lemma for functhinc 48712. 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 725	. . . 4 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → 𝐸 ∈ ThinCat)
3		functhinc.c	. . . 4 ⊢ 𝐶 = (Base‘𝐸)
4		functhinc.j	. . . 4 ⊢ 𝐽 = (Hom ‘𝐸)
5		functhinc.f	. . . . . 6 ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)
6	5	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝐺 = 𝐾) → 𝐹:𝐵⟶𝐶)
7	6	ffvelcdmda 7118	. . . 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 725	. . . . . 6 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → 𝐷 ∈ Cat)
15	10, 11, 12, 14, 9	catidcl 17740	. . . . 5 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → ( 1 ‘𝑎) ∈ (𝑎𝐻𝑎))
16		simplr 768	. . . . . 6 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → 𝐺 = 𝐾)
17		functhinc.k	. . . . . . 7 ⊢ 𝐾 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))))
18		oveq1 7455	. . . . . . . . 9 ⊢ (𝑥 = 𝑣 → (𝑥𝐻𝑦) = (𝑣𝐻𝑦))
19		fveq2 6920	. . . . . . . . . 10 ⊢ (𝑥 = 𝑣 → (𝐹‘𝑥) = (𝐹‘𝑣))
20	19	oveq1d 7463	. . . . . . . . 9 ⊢ (𝑥 = 𝑣 → ((𝐹‘𝑥)𝐽(𝐹‘𝑦)) = ((𝐹‘𝑣)𝐽(𝐹‘𝑦)))
21	18, 20	xpeq12d 5731	. . . . . . . 8 ⊢ (𝑥 = 𝑣 → ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))) = ((𝑣𝐻𝑦) × ((𝐹‘𝑣)𝐽(𝐹‘𝑦))))
22		oveq2 7456	. . . . . . . . 9 ⊢ (𝑦 = 𝑢 → (𝑣𝐻𝑦) = (𝑣𝐻𝑢))
23		fveq2 6920	. . . . . . . . . 10 ⊢ (𝑦 = 𝑢 → (𝐹‘𝑦) = (𝐹‘𝑢))
24	23	oveq2d 7464	. . . . . . . . 9 ⊢ (𝑦 = 𝑢 → ((𝐹‘𝑣)𝐽(𝐹‘𝑦)) = ((𝐹‘𝑣)𝐽(𝐹‘𝑢)))
25	22, 24	xpeq12d 5731	. . . . . . . 8 ⊢ (𝑦 = 𝑢 → ((𝑣𝐻𝑦) × ((𝐹‘𝑣)𝐽(𝐹‘𝑦))) = ((𝑣𝐻𝑢) × ((𝐹‘𝑣)𝐽(𝐹‘𝑢))))
26	21, 25	cbvmpov 7545	. . . . . . 7 ⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) = (𝑣 ∈ 𝐵, 𝑢 ∈ 𝐵 ↦ ((𝑣𝐻𝑢) × ((𝐹‘𝑣)𝐽(𝐹‘𝑢))))
27	17, 26	eqtri 2768	. . . . . 6 ⊢ 𝐾 = (𝑣 ∈ 𝐵, 𝑢 ∈ 𝐵 ↦ ((𝑣𝐻𝑢) × ((𝐹‘𝑣)𝐽(𝐹‘𝑢))))
28	16, 27	eqtrdi 2796	. . . . 5 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → 𝐺 = (𝑣 ∈ 𝐵, 𝑢 ∈ 𝐵 ↦ ((𝑣𝐻𝑢) × ((𝐹‘𝑣)𝐽(𝐹‘𝑢)))))
29		functhinc.1	. . . . . . 7 ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅))
30	29	ad2antrr 725	. . . . . 6 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅))
31	9, 9, 30	functhinclem2 48709	. . . . 5 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → (((𝐹‘𝑎)𝐽(𝐹‘𝑎)) = ∅ → (𝑎𝐻𝑎) = ∅))
32	2, 7, 7, 3, 4	thincmo 48696	. . . . 5 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → ∃*𝑝 𝑝 ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑎)))
33	9, 9, 15, 28, 31, 32	functhinclem3 48710	. . . 4 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → ((𝑎𝐺𝑎)‘( 1 ‘𝑎)) ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑎)))
34	2, 3, 4, 7, 8, 33	thincid 48700	. . 3 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → ((𝑎𝐺𝑎)‘( 1 ‘𝑎)) = (𝐼‘(𝐹‘𝑎)))
35	7	ad2antrr 725	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (𝐹‘𝑎) ∈ 𝐶)
36	5	ad4antr 731	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝐹:𝐵⟶𝐶)
37		simplrr 777	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝑐 ∈ 𝐵)
38	36, 37	ffvelcdmd 7119	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (𝐹‘𝑐) ∈ 𝐶)
39	9	ad2antrr 725	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝑎 ∈ 𝐵)
40		functhinclem4.x	. . . . . . . 8 ⊢ · = (comp‘𝐷)
41	13	ad4antr 731	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝐷 ∈ Cat)
42		simplrl 776	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝑏 ∈ 𝐵)
43		simprl 770	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝑚 ∈ (𝑎𝐻𝑏))
44		simprr 772	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝑛 ∈ (𝑏𝐻𝑐))
45	10, 11, 40, 41, 39, 42, 37, 43, 44	catcocl 17743	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚) ∈ (𝑎𝐻𝑐))
46	28	ad2antrr 725	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝐺 = (𝑣 ∈ 𝐵, 𝑢 ∈ 𝐵 ↦ ((𝑣𝐻𝑢) × ((𝐹‘𝑣)𝐽(𝐹‘𝑢)))))
47	29	ad4antr 731	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅))
48	39, 37, 47	functhinclem2 48709	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (((𝐹‘𝑎)𝐽(𝐹‘𝑐)) = ∅ → (𝑎𝐻𝑐) = ∅))
49	1	ad4antr 731	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝐸 ∈ ThinCat)
50	49, 35, 38, 3, 4	thincmo 48696	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ∃*𝑝 𝑝 ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑐)))
51	39, 37, 45, 46, 48, 50	functhinclem3 48710	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑐)))
52		functhinclem4.o	. . . . . . 7 ⊢ 𝑂 = (comp‘𝐸)
53	2	thinccd 48692	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → 𝐸 ∈ Cat)
54	53	ad2antrr 725	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝐸 ∈ Cat)
55	36, 42	ffvelcdmd 7119	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (𝐹‘𝑏) ∈ 𝐶)
56	39, 42, 47	functhinclem2 48709	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (((𝐹‘𝑎)𝐽(𝐹‘𝑏)) = ∅ → (𝑎𝐻𝑏) = ∅))
57	49, 35, 55, 3, 4	thincmo 48696	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ∃*𝑝 𝑝 ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑏)))
58	39, 42, 43, 46, 56, 57	functhinclem3 48710	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ((𝑎𝐺𝑏)‘𝑚) ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑏)))
59	42, 37, 47	functhinclem2 48709	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (((𝐹‘𝑏)𝐽(𝐹‘𝑐)) = ∅ → (𝑏𝐻𝑐) = ∅))
60	49, 55, 38, 3, 4	thincmo 48696	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ∃*𝑝 𝑝 ∈ ((𝐹‘𝑏)𝐽(𝐹‘𝑐)))
61	42, 37, 44, 46, 59, 60	functhinclem3 48710	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ((𝑏𝐺𝑐)‘𝑛) ∈ ((𝐹‘𝑏)𝐽(𝐹‘𝑐)))
62	3, 4, 52, 54, 35, 55, 38, 58, 61	catcocl 17743	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚)) ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑐)))
63	35, 38, 51, 62, 3, 4, 49	thincmo2 48695	. . . . 5 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) = (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚)))
64	63	ralrimivva 3208	. . . 4 ⊢ ((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → ∀𝑚 ∈ (𝑎𝐻𝑏)∀𝑛 ∈ (𝑏𝐻𝑐)((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) = (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚)))
65	64	ralrimivva 3208	. . 3 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑚 ∈ (𝑎𝐻𝑏)∀𝑛 ∈ (𝑏𝐻𝑐)((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) = (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚)))
66	34, 65	jca 511	. 2 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → (((𝑎𝐺𝑎)‘( 1 ‘𝑎)) = (𝐼‘(𝐹‘𝑎)) ∧ ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑚 ∈ (𝑎𝐻𝑏)∀𝑛 ∈ (𝑏𝐻𝑐)((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) = (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚))))
67	66	ralrimiva 3152	1 ⊢ ((𝜑 ∧ 𝐺 = 𝐾) → ∀𝑎 ∈ 𝐵 (((𝑎𝐺𝑎)‘( 1 ‘𝑎)) = (𝐼‘(𝐹‘𝑎)) ∧ ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑚 ∈ (𝑎𝐻𝑏)∀𝑛 ∈ (𝑏𝐻𝑐)((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) = (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚))))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108  ∀wral 3067  ∅c0 4352  ⟨cop 4654   × cxp 5698  ⟶wf 6569  ‘cfv 6573  (class class class)co 7448   ∈ cmpo 7450  Basecbs 17258  Hom chom 17322  compcco 17323  Catccat 17722  Idccid 17723  ThinCatcthinc 48686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-cat 17726  df-cid 17727  df-thinc 48687

This theorem is referenced by:  functhinc  48712