fcoresf1

Description: If a composition is injective, then the restrictions of its components to the minimum domains are injective. (Contributed by GL and AV, 18-Sep-2024) (Revised by AV, 7-Oct-2024)

	Ref	Expression
Hypotheses	fcores.f	$⊢ φ \to F : A ⟶ B$
	fcores.e	$⊢ E = ran F \cap C$
	fcores.p	$⊢ P = F^{-1} [C]$
	fcores.x	$⊢ X = {F ↾}_{P}$
	fcores.g	$⊢ φ \to G : C ⟶ D$
	fcores.y	$⊢ Y = {G ↾}_{E}$
	fcoresf1.i	$⊢ φ \to (G \circ F) : P \underset{1-1}{⟶} D$
Assertion	fcoresf1	$⊢ φ \to (X : P \underset{1-1}{⟶} E \land Y : E \underset{1-1}{⟶} D)$

Proof

Step	Hyp	Ref	Expression
1		fcores.f	$⊢ φ \to F : A ⟶ B$
2		fcores.e	$⊢ E = ran F \cap C$
3		fcores.p	$⊢ P = F^{-1} [C]$
4		fcores.x	$⊢ X = {F ↾}_{P}$
5		fcores.g	$⊢ φ \to G : C ⟶ D$
6		fcores.y	$⊢ Y = {G ↾}_{E}$
7		fcoresf1.i	$⊢ φ \to (G \circ F) : P \underset{1-1}{⟶} D$
8	1 2 3 4	fcoreslem3	$⊢ φ \to X : P \underset{onto}{⟶} E$
9		fof	$⊢ X : P \underset{onto}{⟶} E \to X : P ⟶ E$
10	8 9	syl	$⊢ φ \to X : P ⟶ E$
11		dff13	$⊢ (G \circ F) : P \underset{1-1}{⟶} D \leftrightarrow ((G \circ F) : P ⟶ D \land \forall x \in P \forall y \in P ((G \circ F) (x) = (G \circ F) (y) \to x = y))$
12	1 2 3 4 5 6	fcoresf1lem	$⊢ (φ \land x \in P) \to (G \circ F) (x) = Y (X (x))$
13	12	adantrr	$⊢ (φ \land (x \in P \land y \in P)) \to (G \circ F) (x) = Y (X (x))$
14	1 2 3 4 5 6	fcoresf1lem	$⊢ (φ \land y \in P) \to (G \circ F) (y) = Y (X (y))$
15	14	adantrl	$⊢ (φ \land (x \in P \land y \in P)) \to (G \circ F) (y) = Y (X (y))$
16	13 15	eqeq12d	$⊢ (φ \land (x \in P \land y \in P)) \to ((G \circ F) (x) = (G \circ F) (y) \leftrightarrow Y (X (x)) = Y (X (y)))$
17	16	imbi1d	$⊢ (φ \land (x \in P \land y \in P)) \to (((G \circ F) (x) = (G \circ F) (y) \to x = y) \leftrightarrow (Y (X (x)) = Y (X (y)) \to x = y))$
18		fveq2	$⊢ X (x) = X (y) \to Y (X (x)) = Y (X (y))$
19	18	a1i	$⊢ (φ \land (x \in P \land y \in P)) \to (X (x) = X (y) \to Y (X (x)) = Y (X (y)))$
20	19	imim1d	$⊢ (φ \land (x \in P \land y \in P)) \to ((Y (X (x)) = Y (X (y)) \to x = y) \to (X (x) = X (y) \to x = y))$
21	17 20	sylbid	$⊢ (φ \land (x \in P \land y \in P)) \to (((G \circ F) (x) = (G \circ F) (y) \to x = y) \to (X (x) = X (y) \to x = y))$
22	21	ralimdvva	$⊢ φ \to (\forall x \in P \forall y \in P ((G \circ F) (x) = (G \circ F) (y) \to x = y) \to \forall x \in P \forall y \in P (X (x) = X (y) \to x = y))$
23	22	adantld	$⊢ φ \to (((G \circ F) : P ⟶ D \land \forall x \in P \forall y \in P ((G \circ F) (x) = (G \circ F) (y) \to x = y)) \to \forall x \in P \forall y \in P (X (x) = X (y) \to x = y))$
24	11 23	syl5bi	$⊢ φ \to ((G \circ F) : P \underset{1-1}{⟶} D \to \forall x \in P \forall y \in P (X (x) = X (y) \to x = y))$
25	7 24	mpd	$⊢ φ \to \forall x \in P \forall y \in P (X (x) = X (y) \to x = y)$
26		dff13	$⊢ X : P \underset{1-1}{⟶} E \leftrightarrow (X : P ⟶ E \land \forall x \in P \forall y \in P (X (x) = X (y) \to x = y))$
27	10 25 26	sylanbrc	$⊢ φ \to X : P \underset{1-1}{⟶} E$
28	2	a1i	$⊢ φ \to E = ran F \cap C$
29		inss2	$⊢ ran F \cap C \subseteq C$
30	28 29	eqsstrdi	$⊢ φ \to E \subseteq C$
31	5 30	fssresd	$⊢ φ \to ({G ↾}_{E}) : E ⟶ D$
32	6	feq1i	$⊢ Y : E ⟶ D \leftrightarrow ({G ↾}_{E}) : E ⟶ D$
33	31 32	sylibr	$⊢ φ \to Y : E ⟶ D$
34	1 2 3 4	fcoreslem2	$⊢ φ \to ran X = E$
35	34	eqcomd	$⊢ φ \to E = ran X$
36	35	eleq2d	$⊢ φ \to (x \in E \leftrightarrow x \in ran X)$
37		fofn	$⊢ X : P \underset{onto}{⟶} E \to X Fn P$
38	8 37	syl	$⊢ φ \to X Fn P$
39		fvelrnb	$⊢ X Fn P \to (x \in ran X \leftrightarrow \exists a \in P X (a) = x)$
40	38 39	syl	$⊢ φ \to (x \in ran X \leftrightarrow \exists a \in P X (a) = x)$
41	36 40	bitrd	$⊢ φ \to (x \in E \leftrightarrow \exists a \in P X (a) = x)$
42	35	eleq2d	$⊢ φ \to (y \in E \leftrightarrow y \in ran X)$
43		fvelrnb	$⊢ X Fn P \to (y \in ran X \leftrightarrow \exists b \in P X (b) = y)$
44	38 43	syl	$⊢ φ \to (y \in ran X \leftrightarrow \exists b \in P X (b) = y)$
45	42 44	bitrd	$⊢ φ \to (y \in E \leftrightarrow \exists b \in P X (b) = y)$
46	41 45	anbi12d	$⊢ φ \to ((x \in E \land y \in E) \leftrightarrow (\exists a \in P X (a) = x \land \exists b \in P X (b) = y))$
47		fveqeq2	$⊢ x = a \to ((G \circ F) (x) = (G \circ F) (y) \leftrightarrow (G \circ F) (a) = (G \circ F) (y))$
48		eqeq1	$⊢ x = a \to (x = y \leftrightarrow a = y)$
49	47 48	imbi12d	$⊢ x = a \to (((G \circ F) (x) = (G \circ F) (y) \to x = y) \leftrightarrow ((G \circ F) (a) = (G \circ F) (y) \to a = y))$
50		fveq2	$⊢ y = b \to (G \circ F) (y) = (G \circ F) (b)$
51	50	eqeq2d	$⊢ y = b \to ((G \circ F) (a) = (G \circ F) (y) \leftrightarrow (G \circ F) (a) = (G \circ F) (b))$
52		equequ2	$⊢ y = b \to (a = y \leftrightarrow a = b)$
53	51 52	imbi12d	$⊢ y = b \to (((G \circ F) (a) = (G \circ F) (y) \to a = y) \leftrightarrow ((G \circ F) (a) = (G \circ F) (b) \to a = b))$
54	49 53	rspc2v	$⊢ (a \in P \land b \in P) \to (\forall x \in P \forall y \in P ((G \circ F) (x) = (G \circ F) (y) \to x = y) \to ((G \circ F) (a) = (G \circ F) (b) \to a = b))$
55	54	adantl	$⊢ (φ \land (a \in P \land b \in P)) \to (\forall x \in P \forall y \in P ((G \circ F) (x) = (G \circ F) (y) \to x = y) \to ((G \circ F) (a) = (G \circ F) (b) \to a = b))$
56	1 2 3 4 5 6	fcoresf1lem	$⊢ (φ \land a \in P) \to (G \circ F) (a) = Y (X (a))$
57	56	adantrr	$⊢ (φ \land (a \in P \land b \in P)) \to (G \circ F) (a) = Y (X (a))$
58	1 2 3 4 5 6	fcoresf1lem	$⊢ (φ \land b \in P) \to (G \circ F) (b) = Y (X (b))$
59	58	adantrl	$⊢ (φ \land (a \in P \land b \in P)) \to (G \circ F) (b) = Y (X (b))$
60	57 59	eqeq12d	$⊢ (φ \land (a \in P \land b \in P)) \to ((G \circ F) (a) = (G \circ F) (b) \leftrightarrow Y (X (a)) = Y (X (b)))$
61	60	imbi1d	$⊢ (φ \land (a \in P \land b \in P)) \to (((G \circ F) (a) = (G \circ F) (b) \to a = b) \leftrightarrow (Y (X (a)) = Y (X (b)) \to a = b))$
62		fveq2	$⊢ a = b \to X (a) = X (b)$
63	62	a1i	$⊢ (φ \land (a \in P \land b \in P)) \to (a = b \to X (a) = X (b))$
64	63	imim2d	$⊢ (φ \land (a \in P \land b \in P)) \to ((Y (X (a)) = Y (X (b)) \to a = b) \to (Y (X (a)) = Y (X (b)) \to X (a) = X (b)))$
65	61 64	sylbid	$⊢ (φ \land (a \in P \land b \in P)) \to (((G \circ F) (a) = (G \circ F) (b) \to a = b) \to (Y (X (a)) = Y (X (b)) \to X (a) = X (b)))$
66	55 65	syld	$⊢ (φ \land (a \in P \land b \in P)) \to (\forall x \in P \forall y \in P ((G \circ F) (x) = (G \circ F) (y) \to x = y) \to (Y (X (a)) = Y (X (b)) \to X (a) = X (b)))$
67	66	ex	$⊢ φ \to ((a \in P \land b \in P) \to (\forall x \in P \forall y \in P ((G \circ F) (x) = (G \circ F) (y) \to x = y) \to (Y (X (a)) = Y (X (b)) \to X (a) = X (b))))$
68	67	com23	$⊢ φ \to (\forall x \in P \forall y \in P ((G \circ F) (x) = (G \circ F) (y) \to x = y) \to ((a \in P \land b \in P) \to (Y (X (a)) = Y (X (b)) \to X (a) = X (b))))$
69	68	adantld	$⊢ φ \to (((G \circ F) : P ⟶ D \land \forall x \in P \forall y \in P ((G \circ F) (x) = (G \circ F) (y) \to x = y)) \to ((a \in P \land b \in P) \to (Y (X (a)) = Y (X (b)) \to X (a) = X (b))))$
70	11 69	syl5bi	$⊢ φ \to ((G \circ F) : P \underset{1-1}{⟶} D \to ((a \in P \land b \in P) \to (Y (X (a)) = Y (X (b)) \to X (a) = X (b))))$
71	7 70	mpd	$⊢ φ \to ((a \in P \land b \in P) \to (Y (X (a)) = Y (X (b)) \to X (a) = X (b)))$
72	71	impl	$⊢ ((φ \land a \in P) \land b \in P) \to (Y (X (a)) = Y (X (b)) \to X (a) = X (b))$
73		fveq2	$⊢ X (a) = x \to Y (X (a)) = Y (x)$
74		fveq2	$⊢ X (b) = y \to Y (X (b)) = Y (y)$
75	73 74	eqeqan12rd	$⊢ (X (b) = y \land X (a) = x) \to (Y (X (a)) = Y (X (b)) \leftrightarrow Y (x) = Y (y))$
76		eqeq12	$⊢ (X (a) = x \land X (b) = y) \to (X (a) = X (b) \leftrightarrow x = y)$
77	76	ancoms	$⊢ (X (b) = y \land X (a) = x) \to (X (a) = X (b) \leftrightarrow x = y)$
78	75 77	imbi12d	$⊢ (X (b) = y \land X (a) = x) \to ((Y (X (a)) = Y (X (b)) \to X (a) = X (b)) \leftrightarrow (Y (x) = Y (y) \to x = y))$
79	72 78	syl5ibcom	$⊢ ((φ \land a \in P) \land b \in P) \to ((X (b) = y \land X (a) = x) \to (Y (x) = Y (y) \to x = y))$
80	79	expd	$⊢ ((φ \land a \in P) \land b \in P) \to (X (b) = y \to (X (a) = x \to (Y (x) = Y (y) \to x = y)))$
81	80	rexlimdva	$⊢ (φ \land a \in P) \to (\exists b \in P X (b) = y \to (X (a) = x \to (Y (x) = Y (y) \to x = y)))$
82	81	com23	$⊢ (φ \land a \in P) \to (X (a) = x \to (\exists b \in P X (b) = y \to (Y (x) = Y (y) \to x = y)))$
83	82	rexlimdva	$⊢ φ \to (\exists a \in P X (a) = x \to (\exists b \in P X (b) = y \to (Y (x) = Y (y) \to x = y)))$
84	83	impd	$⊢ φ \to ((\exists a \in P X (a) = x \land \exists b \in P X (b) = y) \to (Y (x) = Y (y) \to x = y))$
85	46 84	sylbid	$⊢ φ \to ((x \in E \land y \in E) \to (Y (x) = Y (y) \to x = y))$
86	85	ralrimivv	$⊢ φ \to \forall x \in E \forall y \in E (Y (x) = Y (y) \to x = y)$
87		dff13	$⊢ Y : E \underset{1-1}{⟶} D \leftrightarrow (Y : E ⟶ D \land \forall x \in E \forall y \in E (Y (x) = Y (y) \to x = y))$
88	33 86 87	sylanbrc	$⊢ φ \to Y : E \underset{1-1}{⟶} D$
89	27 88	jca	$⊢ φ \to (X : P \underset{1-1}{⟶} E \land Y : E \underset{1-1}{⟶} D)$

Metamath Proof Explorer

Theorem fcoresf1

Proof