functhinclem4 - Mathbox for Zhi Wang

	Mathbox for Zhi Wang		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > functhinclem4		Structured version Visualization version GIF version

Theorem functhinclem4 47664

Description: Lemma for functhinc 47665. 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 482	. . . . 5 ⊢ ((𝜑 ∧ 𝐺 = 𝐾) → 𝐹:𝐵⟶𝐶)
7	6	ffvelcdmda 7087	. . . 4 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → (𝐹‘𝑎) ∈ 𝐶)
8		functhinclem4.i	. . . 4 ⊢ 𝐼 = (Id‘𝐸)
9		simpr 486	. . . . 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 17626	. . . . 5 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → ( 1 ‘𝑎) ∈ (𝑎𝐻𝑎))
16		simplr 768	. . . . . 6 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → 𝐺 = 𝐾)
17		functhinc.k	. . . . . . 7 ⊢ 𝐾 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))))
18		oveq1 7416	. . . . . . . . 9 ⊢ (𝑥 = 𝑣 → (𝑥𝐻𝑦) = (𝑣𝐻𝑦))
19		fveq2 6892	. . . . . . . . . 10 ⊢ (𝑥 = 𝑣 → (𝐹‘𝑥) = (𝐹‘𝑣))
20	19	oveq1d 7424	. . . . . . . . 9 ⊢ (𝑥 = 𝑣 → ((𝐹‘𝑥)𝐽(𝐹‘𝑦)) = ((𝐹‘𝑣)𝐽(𝐹‘𝑦)))
21	18, 20	xpeq12d 5708	. . . . . . . 8 ⊢ (𝑥 = 𝑣 → ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))) = ((𝑣𝐻𝑦) × ((𝐹‘𝑣)𝐽(𝐹‘𝑦))))
22		oveq2 7417	. . . . . . . . 9 ⊢ (𝑦 = 𝑢 → (𝑣𝐻𝑦) = (𝑣𝐻𝑢))
23		fveq2 6892	. . . . . . . . . 10 ⊢ (𝑦 = 𝑢 → (𝐹‘𝑦) = (𝐹‘𝑢))
24	23	oveq2d 7425	. . . . . . . . 9 ⊢ (𝑦 = 𝑢 → ((𝐹‘𝑣)𝐽(𝐹‘𝑦)) = ((𝐹‘𝑣)𝐽(𝐹‘𝑢)))
25	22, 24	xpeq12d 5708	. . . . . . . 8 ⊢ (𝑦 = 𝑢 → ((𝑣𝐻𝑦) × ((𝐹‘𝑣)𝐽(𝐹‘𝑦))) = ((𝑣𝐻𝑢) × ((𝐹‘𝑣)𝐽(𝐹‘𝑢))))
26	21, 25	cbvmpov 7504	. . . . . . 7 ⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) = (𝑣 ∈ 𝐵, 𝑢 ∈ 𝐵 ↦ ((𝑣𝐻𝑢) × ((𝐹‘𝑣)𝐽(𝐹‘𝑢))))
27	17, 26	eqtri 2761	. . . . . 6 ⊢ 𝐾 = (𝑣 ∈ 𝐵, 𝑢 ∈ 𝐵 ↦ ((𝑣𝐻𝑢) × ((𝐹‘𝑣)𝐽(𝐹‘𝑢))))
28	16, 27	eqtrdi 2789	. . . . 5 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → 𝐺 = (𝑣 ∈ 𝐵, 𝑢 ∈ 𝐵 ↦ ((𝑣𝐻𝑢) × ((𝐹‘𝑣)𝐽(𝐹‘𝑢)))))
29		functhinc.1	. . . . . . 7 ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅))
30	29	ad2antrr 725	. . . . . 6 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅))
31	9, 9, 30	functhinclem2 47662	. . . . 5 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → (((𝐹‘𝑎)𝐽(𝐹‘𝑎)) = ∅ → (𝑎𝐻𝑎) = ∅))
32	2, 7, 7, 3, 4	thincmo 47649	. . . . 5 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → ∃*𝑝 𝑝 ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑎)))
33	9, 9, 15, 28, 31, 32	functhinclem3 47663	. . . 4 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → ((𝑎𝐺𝑎)‘( 1 ‘𝑎)) ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑎)))
34	2, 3, 4, 7, 8, 33	thincid 47653	. . 3 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → ((𝑎𝐺𝑎)‘( 1 ‘𝑎)) = (𝐼‘(𝐹‘𝑎)))
35	7	ad2antrr 725	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (𝐹‘𝑎) ∈ 𝐶)
36	5	ad4antr 731	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝐹:𝐵⟶𝐶)
37		simplrr 777	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝑐 ∈ 𝐵)
38	36, 37	ffvelcdmd 7088	. . . . . 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 17629	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚) ∈ (𝑎𝐻𝑐))
46	28	ad2antrr 725	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝐺 = (𝑣 ∈ 𝐵, 𝑢 ∈ 𝐵 ↦ ((𝑣𝐻𝑢) × ((𝐹‘𝑣)𝐽(𝐹‘𝑢)))))
47	29	ad4antr 731	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅))
48	39, 37, 47	functhinclem2 47662	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (((𝐹‘𝑎)𝐽(𝐹‘𝑐)) = ∅ → (𝑎𝐻𝑐) = ∅))
49	1	ad4antr 731	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝐸 ∈ ThinCat)
50	49, 35, 38, 3, 4	thincmo 47649	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ∃*𝑝 𝑝 ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑐)))
51	39, 37, 45, 46, 48, 50	functhinclem3 47663	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑐)))
52		functhinclem4.o	. . . . . . 7 ⊢ 𝑂 = (comp‘𝐸)
53	2	thinccd 47645	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → 𝐸 ∈ Cat)
54	53	ad2antrr 725	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → 𝐸 ∈ Cat)
55	36, 42	ffvelcdmd 7088	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (𝐹‘𝑏) ∈ 𝐶)
56	39, 42, 47	functhinclem2 47662	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (((𝐹‘𝑎)𝐽(𝐹‘𝑏)) = ∅ → (𝑎𝐻𝑏) = ∅))
57	49, 35, 55, 3, 4	thincmo 47649	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ∃*𝑝 𝑝 ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑏)))
58	39, 42, 43, 46, 56, 57	functhinclem3 47663	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ((𝑎𝐺𝑏)‘𝑚) ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑏)))
59	42, 37, 47	functhinclem2 47662	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (((𝐹‘𝑏)𝐽(𝐹‘𝑐)) = ∅ → (𝑏𝐻𝑐) = ∅))
60	49, 55, 38, 3, 4	thincmo 47649	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ∃*𝑝 𝑝 ∈ ((𝐹‘𝑏)𝐽(𝐹‘𝑐)))
61	42, 37, 44, 46, 59, 60	functhinclem3 47663	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ((𝑏𝐺𝑐)‘𝑛) ∈ ((𝐹‘𝑏)𝐽(𝐹‘𝑐)))
62	3, 4, 52, 54, 35, 55, 38, 58, 61	catcocl 17629	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚)) ∈ ((𝐹‘𝑎)𝐽(𝐹‘𝑐)))
63	35, 38, 51, 62, 3, 4, 49	thincmo2 47648	. . . . 5 ⊢ (((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑚 ∈ (𝑎𝐻𝑏) ∧ 𝑛 ∈ (𝑏𝐻𝑐))) → ((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) = (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚)))
64	63	ralrimivva 3201	. . . 4 ⊢ ((((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → ∀𝑚 ∈ (𝑎𝐻𝑏)∀𝑛 ∈ (𝑏𝐻𝑐)((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) = (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚)))
65	64	ralrimivva 3201	. . 3 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑚 ∈ (𝑎𝐻𝑏)∀𝑛 ∈ (𝑏𝐻𝑐)((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) = (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚)))
66	34, 65	jca 513	. 2 ⊢ (((𝜑 ∧ 𝐺 = 𝐾) ∧ 𝑎 ∈ 𝐵) → (((𝑎𝐺𝑎)‘( 1 ‘𝑎)) = (𝐼‘(𝐹‘𝑎)) ∧ ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑚 ∈ (𝑎𝐻𝑏)∀𝑛 ∈ (𝑏𝐻𝑐)((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) = (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚))))
67	66	ralrimiva 3147	1 ⊢ ((𝜑 ∧ 𝐺 = 𝐾) → ∀𝑎 ∈ 𝐵 (((𝑎𝐺𝑎)‘( 1 ‘𝑎)) = (𝐼‘(𝐹‘𝑎)) ∧ ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑚 ∈ (𝑎𝐻𝑏)∀𝑛 ∈ (𝑏𝐻𝑐)((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) = (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ∀wral 3062 ∅c0 4323 ⟨cop 4635 × cxp 5675 ⟶wf 6540 ‘cfv 6544 (class class class)co 7409 ∈ cmpo 7411 Basecbs 17144 Hom chom 17208 compcco 17209 Catccat 17608 Idccid 17609 ThinCatcthinc 47639

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-riota 7365 df-ov 7412 df-oprab 7413 df-mpo 7414 df-cat 17612 df-cid 17613 df-thinc 47640

This theorem is referenced by: functhinc 47665

W3C validator