f1cof1blem

Description: Lemma for f1cof1b and focofob . (Contributed by AV, 18-Sep-2024)

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		f1cof1blem.s	$⊢ φ \to ran F = C$
8	7	eqcomd	$⊢ φ \to C = ran F$
9	8	imaeq2d	$⊢ φ \to F^{-1} [C] = F^{-1} [ran F]$
10	3 9	syl5eq	$⊢ φ \to P = F^{-1} [ran F]$
11		cnvimarndm	$⊢ F^{-1} [ran F] = dom F$
12	1	fdmd	$⊢ φ \to dom F = A$
13	11 12	syl5eq	$⊢ φ \to F^{-1} [ran F] = A$
14	10 13	eqtrd	$⊢ φ \to P = A$
15		simpr	$⊢ (φ \land ran F = C) \to ran F = C$
16	15	ineq1d	$⊢ (φ \land ran F = C) \to ran F \cap C = C \cap C$
17		inidm	$⊢ C \cap C = C$
18	16 17	eqtrdi	$⊢ (φ \land ran F = C) \to ran F \cap C = C$
19	7 18	mpdan	$⊢ φ \to ran F \cap C = C$
20	2 19	syl5eq	$⊢ φ \to E = C$
21	14 20	jca	$⊢ φ \to (P = A \land E = C)$
22	10 11	eqtrdi	$⊢ φ \to P = dom F$
23	22	reseq2d	$⊢ φ \to {F ↾}_{P} = {F ↾}_{dom F}$
24	4 23	syl5eq	$⊢ φ \to X = {F ↾}_{dom F}$
25	1	freld	$⊢ φ \to Rel F$
26		resdm	$⊢ Rel F \to {F ↾}_{dom F} = F$
27	25 26	syl	$⊢ φ \to {F ↾}_{dom F} = F$
28	24 27	eqtrd	$⊢ φ \to X = F$
29	5	fdmd	$⊢ φ \to dom G = C$
30	20 29	eqtr4d	$⊢ φ \to E = dom G$
31	30	reseq2d	$⊢ φ \to {G ↾}_{E} = {G ↾}_{dom G}$
32	6 31	syl5eq	$⊢ φ \to Y = {G ↾}_{dom G}$
33	5	freld	$⊢ φ \to Rel G$
34		resdm	$⊢ Rel G \to {G ↾}_{dom G} = G$
35	33 34	syl	$⊢ φ \to {G ↾}_{dom G} = G$
36	32 35	eqtrd	$⊢ φ \to Y = G$
37	21 28 36	jca32	$⊢ φ \to ((P = A \land E = C) \land (X = F \land Y = G))$

Metamath Proof Explorer