imaf1co

Description: An image of a functor whose object part is injective preserves the composition. (Contributed by Zhi Wang, 7-Nov-2025)

	Ref	Expression
Hypotheses	imasubc.s	$⊢ S = F [A]$
	imasubc.h	$⊢ H = Hom (D)$
	imasubc.k	$⊢ K = (x \in S, y \in S ⟼ ⋃_{p \in F^{-1} [\{x\}] \times F^{-1} [\{y\}]} G (p) [H (p)])$
	imassc.f	$⊢ φ \to F (D Func E) G$
	imaf1co.b	$⊢ B = {Base}_{D}$
	imaf1co.c	$⊢ C = {Base}_{E}$
	imaf1co.o	$⊢ \underset{˙}{∙} = comp (E)$
	imaf1co.f	$⊢ φ \to F : B \underset{1-1}{⟶} C$
	imaf1co.x	$⊢ φ \to X \in S$
	imaf1co.y	$⊢ φ \to Y \in S$
	imaf1co.z	$⊢ φ \to Z \in S$
	imaf1co.m	$⊢ φ \to M \in (X K Y)$
	imaf1co.n	$⊢ φ \to N \in (Y K Z)$
Assertion	imaf1co	$⊢ φ \to N (⟨X, Y⟩ \underset{˙}{∙} Z) M \in (X K Z)$

Proof

Step	Hyp	Ref	Expression
1		imasubc.s	$⊢ S = F [A]$
2		imasubc.h	$⊢ H = Hom (D)$
3		imasubc.k	$⊢ K = (x \in S, y \in S ⟼ ⋃_{p \in F^{-1} [\{x\}] \times F^{-1} [\{y\}]} G (p) [H (p)])$
4		imassc.f	$⊢ φ \to F (D Func E) G$
5		imaf1co.b	$⊢ B = {Base}_{D}$
6		imaf1co.c	$⊢ C = {Base}_{E}$
7		imaf1co.o	$⊢ \underset{˙}{∙} = comp (E)$
8		imaf1co.f	$⊢ φ \to F : B \underset{1-1}{⟶} C$
9		imaf1co.x	$⊢ φ \to X \in S$
10		imaf1co.y	$⊢ φ \to Y \in S$
11		imaf1co.z	$⊢ φ \to Z \in S$
12		imaf1co.m	$⊢ φ \to M \in (X K Y)$
13		imaf1co.n	$⊢ φ \to N \in (Y K Z)$
14		eqid	$⊢ comp (D) = comp (D)$
15	4	funcrcl2	$⊢ φ \to D \in Cat$
16	15	ad4antr	$⊢ ((((φ \land m \in (F^{-1} (X) H F^{-1} (Y))) \land (F^{-1} (X) G F^{-1} (Y)) (m) = M) \land n \in (F^{-1} (Y) H F^{-1} (Z))) \land (F^{-1} (Y) G F^{-1} (Z)) (n) = N) \to D \in Cat$
17	1 8 9	imaf1homlem	$⊢ φ \to (\{F^{-1} (X)\} = F^{-1} [\{X\}] \land F (F^{-1} (X)) = X \land F^{-1} (X) \in B)$
18	17	simp3d	$⊢ φ \to F^{-1} (X) \in B$
19	18	ad4antr	$⊢ ((((φ \land m \in (F^{-1} (X) H F^{-1} (Y))) \land (F^{-1} (X) G F^{-1} (Y)) (m) = M) \land n \in (F^{-1} (Y) H F^{-1} (Z))) \land (F^{-1} (Y) G F^{-1} (Z)) (n) = N) \to F^{-1} (X) \in B$
20	1 8 10	imaf1homlem	$⊢ φ \to (\{F^{-1} (Y)\} = F^{-1} [\{Y\}] \land F (F^{-1} (Y)) = Y \land F^{-1} (Y) \in B)$
21	20	simp3d	$⊢ φ \to F^{-1} (Y) \in B$
22	21	ad4antr	$⊢ ((((φ \land m \in (F^{-1} (X) H F^{-1} (Y))) \land (F^{-1} (X) G F^{-1} (Y)) (m) = M) \land n \in (F^{-1} (Y) H F^{-1} (Z))) \land (F^{-1} (Y) G F^{-1} (Z)) (n) = N) \to F^{-1} (Y) \in B$
23	1 8 11	imaf1homlem	$⊢ φ \to (\{F^{-1} (Z)\} = F^{-1} [\{Z\}] \land F (F^{-1} (Z)) = Z \land F^{-1} (Z) \in B)$
24	23	simp3d	$⊢ φ \to F^{-1} (Z) \in B$
25	24	ad4antr	$⊢ ((((φ \land m \in (F^{-1} (X) H F^{-1} (Y))) \land (F^{-1} (X) G F^{-1} (Y)) (m) = M) \land n \in (F^{-1} (Y) H F^{-1} (Z))) \land (F^{-1} (Y) G F^{-1} (Z)) (n) = N) \to F^{-1} (Z) \in B$
26		simp-4r	$⊢ ((((φ \land m \in (F^{-1} (X) H F^{-1} (Y))) \land (F^{-1} (X) G F^{-1} (Y)) (m) = M) \land n \in (F^{-1} (Y) H F^{-1} (Z))) \land (F^{-1} (Y) G F^{-1} (Z)) (n) = N) \to m \in (F^{-1} (X) H F^{-1} (Y))$
27		simplr	$⊢ ((((φ \land m \in (F^{-1} (X) H F^{-1} (Y))) \land (F^{-1} (X) G F^{-1} (Y)) (m) = M) \land n \in (F^{-1} (Y) H F^{-1} (Z))) \land (F^{-1} (Y) G F^{-1} (Z)) (n) = N) \to n \in (F^{-1} (Y) H F^{-1} (Z))$
28	5 2 14 16 19 22 25 26 27	catcocl	$⊢ ((((φ \land m \in (F^{-1} (X) H F^{-1} (Y))) \land (F^{-1} (X) G F^{-1} (Y)) (m) = M) \land n \in (F^{-1} (Y) H F^{-1} (Z))) \land (F^{-1} (Y) G F^{-1} (Z)) (n) = N) \to n (⟨F^{-1} (X), F^{-1} (Y)⟩ comp (D) F^{-1} (Z)) m \in (F^{-1} (X) H F^{-1} (Z))$
29		eqid	$⊢ Hom (E) = Hom (E)$
30	5 2 29 4 18 24	funcf2	$⊢ φ \to (F^{-1} (X) G F^{-1} (Z)) : F^{-1} (X) H F^{-1} (Z) ⟶ F (F^{-1} (X)) Hom (E) F (F^{-1} (Z))$
31	30	ad4antr	$⊢ ((((φ \land m \in (F^{-1} (X) H F^{-1} (Y))) \land (F^{-1} (X) G F^{-1} (Y)) (m) = M) \land n \in (F^{-1} (Y) H F^{-1} (Z))) \land (F^{-1} (Y) G F^{-1} (Z)) (n) = N) \to (F^{-1} (X) G F^{-1} (Z)) : F^{-1} (X) H F^{-1} (Z) ⟶ F (F^{-1} (X)) Hom (E) F (F^{-1} (Z))$
32	31	funfvima2d	$⊢ (((((φ \land m \in (F^{-1} (X) H F^{-1} (Y))) \land (F^{-1} (X) G F^{-1} (Y)) (m) = M) \land n \in (F^{-1} (Y) H F^{-1} (Z))) \land (F^{-1} (Y) G F^{-1} (Z)) (n) = N) \land n (⟨F^{-1} (X), F^{-1} (Y)⟩ comp (D) F^{-1} (Z)) m \in (F^{-1} (X) H F^{-1} (Z))) \to (F^{-1} (X) G F^{-1} (Z)) (n (⟨F^{-1} (X), F^{-1} (Y)⟩ comp (D) F^{-1} (Z)) m) \in (F^{-1} (X) G F^{-1} (Z)) [F^{-1} (X) H F^{-1} (Z)]$
33	28 32	mpdan	$⊢ ((((φ \land m \in (F^{-1} (X) H F^{-1} (Y))) \land (F^{-1} (X) G F^{-1} (Y)) (m) = M) \land n \in (F^{-1} (Y) H F^{-1} (Z))) \land (F^{-1} (Y) G F^{-1} (Z)) (n) = N) \to (F^{-1} (X) G F^{-1} (Z)) (n (⟨F^{-1} (X), F^{-1} (Y)⟩ comp (D) F^{-1} (Z)) m) \in (F^{-1} (X) G F^{-1} (Z)) [F^{-1} (X) H F^{-1} (Z)]$
34	4	ad4antr	$⊢ ((((φ \land m \in (F^{-1} (X) H F^{-1} (Y))) \land (F^{-1} (X) G F^{-1} (Y)) (m) = M) \land n \in (F^{-1} (Y) H F^{-1} (Z))) \land (F^{-1} (Y) G F^{-1} (Z)) (n) = N) \to F (D Func E) G$
35	5 2 14 7 34 19 22 25 26 27	funcco	$⊢ ((((φ \land m \in (F^{-1} (X) H F^{-1} (Y))) \land (F^{-1} (X) G F^{-1} (Y)) (m) = M) \land n \in (F^{-1} (Y) H F^{-1} (Z))) \land (F^{-1} (Y) G F^{-1} (Z)) (n) = N) \to (F^{-1} (X) G F^{-1} (Z)) (n (⟨F^{-1} (X), F^{-1} (Y)⟩ comp (D) F^{-1} (Z)) m) = (F^{-1} (Y) G F^{-1} (Z)) (n) (⟨F (F^{-1} (X)), F (F^{-1} (Y))⟩ \underset{˙}{∙} F (F^{-1} (Z))) (F^{-1} (X) G F^{-1} (Y)) (m)$
36	17	simp2d	$⊢ φ \to F (F^{-1} (X)) = X$
37	36	ad4antr	$⊢ ((((φ \land m \in (F^{-1} (X) H F^{-1} (Y))) \land (F^{-1} (X) G F^{-1} (Y)) (m) = M) \land n \in (F^{-1} (Y) H F^{-1} (Z))) \land (F^{-1} (Y) G F^{-1} (Z)) (n) = N) \to F (F^{-1} (X)) = X$
38	20	simp2d	$⊢ φ \to F (F^{-1} (Y)) = Y$
39	38	ad4antr	$⊢ ((((φ \land m \in (F^{-1} (X) H F^{-1} (Y))) \land (F^{-1} (X) G F^{-1} (Y)) (m) = M) \land n \in (F^{-1} (Y) H F^{-1} (Z))) \land (F^{-1} (Y) G F^{-1} (Z)) (n) = N) \to F (F^{-1} (Y)) = Y$
40	37 39	opeq12d	$⊢ ((((φ \land m \in (F^{-1} (X) H F^{-1} (Y))) \land (F^{-1} (X) G F^{-1} (Y)) (m) = M) \land n \in (F^{-1} (Y) H F^{-1} (Z))) \land (F^{-1} (Y) G F^{-1} (Z)) (n) = N) \to ⟨F (F^{-1} (X)), F (F^{-1} (Y))⟩ = ⟨X, Y⟩$
41	23	simp2d	$⊢ φ \to F (F^{-1} (Z)) = Z$
42	41	ad4antr	$⊢ ((((φ \land m \in (F^{-1} (X) H F^{-1} (Y))) \land (F^{-1} (X) G F^{-1} (Y)) (m) = M) \land n \in (F^{-1} (Y) H F^{-1} (Z))) \land (F^{-1} (Y) G F^{-1} (Z)) (n) = N) \to F (F^{-1} (Z)) = Z$
43	40 42	oveq12d	$⊢ ((((φ \land m \in (F^{-1} (X) H F^{-1} (Y))) \land (F^{-1} (X) G F^{-1} (Y)) (m) = M) \land n \in (F^{-1} (Y) H F^{-1} (Z))) \land (F^{-1} (Y) G F^{-1} (Z)) (n) = N) \to ⟨F (F^{-1} (X)), F (F^{-1} (Y))⟩ \underset{˙}{∙} F (F^{-1} (Z)) = ⟨X, Y⟩ \underset{˙}{∙} Z$
44		simpr	$⊢ ((((φ \land m \in (F^{-1} (X) H F^{-1} (Y))) \land (F^{-1} (X) G F^{-1} (Y)) (m) = M) \land n \in (F^{-1} (Y) H F^{-1} (Z))) \land (F^{-1} (Y) G F^{-1} (Z)) (n) = N) \to (F^{-1} (Y) G F^{-1} (Z)) (n) = N$
45		simpllr	$⊢ ((((φ \land m \in (F^{-1} (X) H F^{-1} (Y))) \land (F^{-1} (X) G F^{-1} (Y)) (m) = M) \land n \in (F^{-1} (Y) H F^{-1} (Z))) \land (F^{-1} (Y) G F^{-1} (Z)) (n) = N) \to (F^{-1} (X) G F^{-1} (Y)) (m) = M$
46	43 44 45	oveq123d	$⊢ ((((φ \land m \in (F^{-1} (X) H F^{-1} (Y))) \land (F^{-1} (X) G F^{-1} (Y)) (m) = M) \land n \in (F^{-1} (Y) H F^{-1} (Z))) \land (F^{-1} (Y) G F^{-1} (Z)) (n) = N) \to (F^{-1} (Y) G F^{-1} (Z)) (n) (⟨F (F^{-1} (X)), F (F^{-1} (Y))⟩ \underset{˙}{∙} F (F^{-1} (Z))) (F^{-1} (X) G F^{-1} (Y)) (m) = N (⟨X, Y⟩ \underset{˙}{∙} Z) M$
47	35 46	eqtr2d	$⊢ ((((φ \land m \in (F^{-1} (X) H F^{-1} (Y))) \land (F^{-1} (X) G F^{-1} (Y)) (m) = M) \land n \in (F^{-1} (Y) H F^{-1} (Z))) \land (F^{-1} (Y) G F^{-1} (Z)) (n) = N) \to N (⟨X, Y⟩ \underset{˙}{∙} Z) M = (F^{-1} (X) G F^{-1} (Z)) (n (⟨F^{-1} (X), F^{-1} (Y)⟩ comp (D) F^{-1} (Z)) m)$
48		relfunc	$⊢ Rel (D Func E)$
49	48	brrelex1i	$⊢ F (D Func E) G \to F \in V$
50	4 49	syl	$⊢ φ \to F \in V$
51	1 8 9 11 50 3	imaf1hom	$⊢ φ \to X K Z = (F^{-1} (X) G F^{-1} (Z)) [F^{-1} (X) H F^{-1} (Z)]$
52	51	ad4antr	$⊢ ((((φ \land m \in (F^{-1} (X) H F^{-1} (Y))) \land (F^{-1} (X) G F^{-1} (Y)) (m) = M) \land n \in (F^{-1} (Y) H F^{-1} (Z))) \land (F^{-1} (Y) G F^{-1} (Z)) (n) = N) \to X K Z = (F^{-1} (X) G F^{-1} (Z)) [F^{-1} (X) H F^{-1} (Z)]$
53	33 47 52	3eltr4d	$⊢ ((((φ \land m \in (F^{-1} (X) H F^{-1} (Y))) \land (F^{-1} (X) G F^{-1} (Y)) (m) = M) \land n \in (F^{-1} (Y) H F^{-1} (Z))) \land (F^{-1} (Y) G F^{-1} (Z)) (n) = N) \to N (⟨X, Y⟩ \underset{˙}{∙} Z) M \in (X K Z)$
54	5 2 29 4 21 24	funcf2	$⊢ φ \to (F^{-1} (Y) G F^{-1} (Z)) : F^{-1} (Y) H F^{-1} (Z) ⟶ F (F^{-1} (Y)) Hom (E) F (F^{-1} (Z))$
55	54	ffund	$⊢ φ \to Fun (F^{-1} (Y) G F^{-1} (Z))$
56	1 8 10 11 50 3	imaf1hom	$⊢ φ \to Y K Z = (F^{-1} (Y) G F^{-1} (Z)) [F^{-1} (Y) H F^{-1} (Z)]$
57	13 56	eleqtrd	$⊢ φ \to N \in (F^{-1} (Y) G F^{-1} (Z)) [F^{-1} (Y) H F^{-1} (Z)]$
58		fvelima	$⊢ (Fun (F^{-1} (Y) G F^{-1} (Z)) \land N \in (F^{-1} (Y) G F^{-1} (Z)) [F^{-1} (Y) H F^{-1} (Z)]) \to \exists n \in (F^{-1} (Y) H F^{-1} (Z)) (F^{-1} (Y) G F^{-1} (Z)) (n) = N$
59	55 57 58	syl2anc	$⊢ φ \to \exists n \in (F^{-1} (Y) H F^{-1} (Z)) (F^{-1} (Y) G F^{-1} (Z)) (n) = N$
60	59	ad2antrr	$⊢ ((φ \land m \in (F^{-1} (X) H F^{-1} (Y))) \land (F^{-1} (X) G F^{-1} (Y)) (m) = M) \to \exists n \in (F^{-1} (Y) H F^{-1} (Z)) (F^{-1} (Y) G F^{-1} (Z)) (n) = N$
61	53 60	r19.29a	$⊢ ((φ \land m \in (F^{-1} (X) H F^{-1} (Y))) \land (F^{-1} (X) G F^{-1} (Y)) (m) = M) \to N (⟨X, Y⟩ \underset{˙}{∙} Z) M \in (X K Z)$
62	5 2 29 4 18 21	funcf2	$⊢ φ \to (F^{-1} (X) G F^{-1} (Y)) : F^{-1} (X) H F^{-1} (Y) ⟶ F (F^{-1} (X)) Hom (E) F (F^{-1} (Y))$
63	62	ffund	$⊢ φ \to Fun (F^{-1} (X) G F^{-1} (Y))$
64	1 8 9 10 50 3	imaf1hom	$⊢ φ \to X K Y = (F^{-1} (X) G F^{-1} (Y)) [F^{-1} (X) H F^{-1} (Y)]$
65	12 64	eleqtrd	$⊢ φ \to M \in (F^{-1} (X) G F^{-1} (Y)) [F^{-1} (X) H F^{-1} (Y)]$
66		fvelima	$⊢ (Fun (F^{-1} (X) G F^{-1} (Y)) \land M \in (F^{-1} (X) G F^{-1} (Y)) [F^{-1} (X) H F^{-1} (Y)]) \to \exists m \in (F^{-1} (X) H F^{-1} (Y)) (F^{-1} (X) G F^{-1} (Y)) (m) = M$
67	63 65 66	syl2anc	$⊢ φ \to \exists m \in (F^{-1} (X) H F^{-1} (Y)) (F^{-1} (X) G F^{-1} (Y)) (m) = M$
68	61 67	r19.29a	$⊢ φ \to N (⟨X, Y⟩ \underset{˙}{∙} Z) M \in (X K Z)$

Metamath Proof Explorer

Theorem imaf1co

Proof