Theorem f1cof1blem

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

	Ref	Expression
Hypotheses	fcores.f	|- ( ph -> F : A --> B )
	fcores.e	|- E = ( ran F i^i C )
	fcores.p	|- P = ( `' F " C )
	fcores.x	|- X = ( F |` P )
	fcores.g	|- ( ph -> G : C --> D )
	fcores.y	|- Y = ( G |` E )
	f1cof1blem.s	|- ( ph -> ran F = C )
Assertion	f1cof1blem	|- ( ph -> ( ( P = A /\ E = C ) /\ ( X = F /\ Y = G ) ) )

Proof

Step	Hyp	Ref	Expression
1		fcores.f	|- ( ph -> F : A --> B )
2		fcores.e	|- E = ( ran F i^i C )
3		fcores.p	|- P = ( `' F " C )
4		fcores.x	|- X = ( F |` P )
5		fcores.g	|- ( ph -> G : C --> D )
6		fcores.y	|- Y = ( G |` E )
7		f1cof1blem.s	|- ( ph -> ran F = C )
8	7	eqcomd	|- ( ph -> C = ran F )
9	8	imaeq2d	|- ( ph -> ( `' F " C ) = ( `' F " ran F ) )
10	3 9	syl5eq	|- ( ph -> P = ( `' F " ran F ) )
11		cnvimarndm	|- ( `' F " ran F ) = dom F
12	1	fdmd	|- ( ph -> dom F = A )
13	11 12	syl5eq	|- ( ph -> ( `' F " ran F ) = A )
14	10 13	eqtrd	|- ( ph -> P = A )
15		simpr	|- ( ( ph /\ ran F = C ) -> ran F = C )
16	15	ineq1d	|- ( ( ph /\ ran F = C ) -> ( ran F i^i C ) = ( C i^i C ) )
17		inidm	|- ( C i^i C ) = C
18	16 17	eqtrdi	|- ( ( ph /\ ran F = C ) -> ( ran F i^i C ) = C )
19	7 18	mpdan	|- ( ph -> ( ran F i^i C ) = C )
20	2 19	syl5eq	|- ( ph -> E = C )
21	14 20	jca	|- ( ph -> ( P = A /\ E = C ) )
22	10 11	eqtrdi	|- ( ph -> P = dom F )
23	22	reseq2d	|- ( ph -> ( F |` P ) = ( F |` dom F ) )
24	4 23	syl5eq	|- ( ph -> X = ( F |` dom F ) )
25	1	freld	|- ( ph -> Rel F )
26		resdm	|- ( Rel F -> ( F |` dom F ) = F )
27	25 26	syl	|- ( ph -> ( F |` dom F ) = F )
28	24 27	eqtrd	|- ( ph -> X = F )
29	5	fdmd	|- ( ph -> dom G = C )
30	20 29	eqtr4d	|- ( ph -> E = dom G )
31	30	reseq2d	|- ( ph -> ( G |` E ) = ( G |` dom G ) )
32	6 31	syl5eq	|- ( ph -> Y = ( G |` dom G ) )
33	5	freld	|- ( ph -> Rel G )
34		resdm	|- ( Rel G -> ( G |` dom G ) = G )
35	33 34	syl	|- ( ph -> ( G |` dom G ) = G )
36	32 35	eqtrd	|- ( ph -> Y = G )
37	21 28 36	jca32	|- ( ph -> ( ( P = A /\ E = C ) /\ ( X = F /\ Y = G ) ) )