Theorem f1cof1blem

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

	Ref	Expression
Hypotheses	fcores.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	fcores.e	⊢ 𝐸 = ( ran 𝐹 ∩ 𝐶 )
	fcores.p	⊢ 𝑃 = ( ◡ 𝐹 “ 𝐶 )
	fcores.x	⊢ 𝑋 = ( 𝐹 ↾ 𝑃 )
	fcores.g	⊢ ( 𝜑 → 𝐺 : 𝐶 ⟶ 𝐷 )
	fcores.y	⊢ 𝑌 = ( 𝐺 ↾ 𝐸 )
	f1cof1blem.s	⊢ ( 𝜑 → ran 𝐹 = 𝐶 )
Assertion	f1cof1blem	⊢ ( 𝜑 → ( ( 𝑃 = 𝐴 ∧ 𝐸 = 𝐶 ) ∧ ( 𝑋 = 𝐹 ∧ 𝑌 = 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fcores.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2		fcores.e	⊢ 𝐸 = ( ran 𝐹 ∩ 𝐶 )
3		fcores.p	⊢ 𝑃 = ( ◡ 𝐹 “ 𝐶 )
4		fcores.x	⊢ 𝑋 = ( 𝐹 ↾ 𝑃 )
5		fcores.g	⊢ ( 𝜑 → 𝐺 : 𝐶 ⟶ 𝐷 )
6		fcores.y	⊢ 𝑌 = ( 𝐺 ↾ 𝐸 )
7		f1cof1blem.s	⊢ ( 𝜑 → ran 𝐹 = 𝐶 )
8	7	eqcomd	⊢ ( 𝜑 → 𝐶 = ran 𝐹 )
9	8	imaeq2d	⊢ ( 𝜑 → ( ◡ 𝐹 “ 𝐶 ) = ( ◡ 𝐹 “ ran 𝐹 ) )
10	3 9	syl5eq	⊢ ( 𝜑 → 𝑃 = ( ◡ 𝐹 “ ran 𝐹 ) )
11		cnvimarndm	⊢ ( ◡ 𝐹 “ ran 𝐹 ) = dom 𝐹
12	1	fdmd	⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
13	11 12	syl5eq	⊢ ( 𝜑 → ( ◡ 𝐹 “ ran 𝐹 ) = 𝐴 )
14	10 13	eqtrd	⊢ ( 𝜑 → 𝑃 = 𝐴 )
15		simpr	⊢ ( ( 𝜑 ∧ ran 𝐹 = 𝐶 ) → ran 𝐹 = 𝐶 )
16	15	ineq1d	⊢ ( ( 𝜑 ∧ ran 𝐹 = 𝐶 ) → ( ran 𝐹 ∩ 𝐶 ) = ( 𝐶 ∩ 𝐶 ) )
17		inidm	⊢ ( 𝐶 ∩ 𝐶 ) = 𝐶
18	16 17	eqtrdi	⊢ ( ( 𝜑 ∧ ran 𝐹 = 𝐶 ) → ( ran 𝐹 ∩ 𝐶 ) = 𝐶 )
19	7 18	mpdan	⊢ ( 𝜑 → ( ran 𝐹 ∩ 𝐶 ) = 𝐶 )
20	2 19	syl5eq	⊢ ( 𝜑 → 𝐸 = 𝐶 )
21	14 20	jca	⊢ ( 𝜑 → ( 𝑃 = 𝐴 ∧ 𝐸 = 𝐶 ) )
22	10 11	eqtrdi	⊢ ( 𝜑 → 𝑃 = dom 𝐹 )
23	22	reseq2d	⊢ ( 𝜑 → ( 𝐹 ↾ 𝑃 ) = ( 𝐹 ↾ dom 𝐹 ) )
24	4 23	syl5eq	⊢ ( 𝜑 → 𝑋 = ( 𝐹 ↾ dom 𝐹 ) )
25	1	freld	⊢ ( 𝜑 → Rel 𝐹 )
26		resdm	⊢ ( Rel 𝐹 → ( 𝐹 ↾ dom 𝐹 ) = 𝐹 )
27	25 26	syl	⊢ ( 𝜑 → ( 𝐹 ↾ dom 𝐹 ) = 𝐹 )
28	24 27	eqtrd	⊢ ( 𝜑 → 𝑋 = 𝐹 )
29	5	fdmd	⊢ ( 𝜑 → dom 𝐺 = 𝐶 )
30	20 29	eqtr4d	⊢ ( 𝜑 → 𝐸 = dom 𝐺 )
31	30	reseq2d	⊢ ( 𝜑 → ( 𝐺 ↾ 𝐸 ) = ( 𝐺 ↾ dom 𝐺 ) )
32	6 31	syl5eq	⊢ ( 𝜑 → 𝑌 = ( 𝐺 ↾ dom 𝐺 ) )
33	5	freld	⊢ ( 𝜑 → Rel 𝐺 )
34		resdm	⊢ ( Rel 𝐺 → ( 𝐺 ↾ dom 𝐺 ) = 𝐺 )
35	33 34	syl	⊢ ( 𝜑 → ( 𝐺 ↾ dom 𝐺 ) = 𝐺 )
36	32 35	eqtrd	⊢ ( 𝜑 → 𝑌 = 𝐺 )
37	21 28 36	jca32	⊢ ( 𝜑 → ( ( 𝑃 = 𝐴 ∧ 𝐸 = 𝐶 ) ∧ ( 𝑋 = 𝐹 ∧ 𝑌 = 𝐺 ) ) )