This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝜑 → 𝑃 = ( ◡ 𝐹 “ ran 𝐹 ) )
11 cnvimarndm ⊢ ( ◡ 𝐹 “ ran 𝐹 ) = dom 𝐹
12 1 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
13 11 12 eqtrid ⊢ ( 𝜑 → ( ◡ 𝐹 “ 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 eqtrid ⊢ ( 𝜑 → 𝐸 = 𝐶 )
21 14 20 jca ⊢ ( 𝜑 → ( 𝑃 = 𝐴 ∧ 𝐸 = 𝐶 ) )
22 10 11 eqtrdi ⊢ ( 𝜑 → 𝑃 = dom 𝐹 )
23 22 reseq2d ⊢ ( 𝜑 → ( 𝐹 ↾ 𝑃 ) = ( 𝐹 ↾ dom 𝐹 ) )
24 4 23 eqtrid ⊢ ( 𝜑 → 𝑋 = ( 𝐹 ↾ 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 eqtrid ⊢ ( 𝜑 → 𝑌 = ( 𝐺 ↾ dom 𝐺 ) )
33 5 freld ⊢ ( 𝜑 → Rel 𝐺 )
34 resdm ⊢ ( Rel 𝐺 → ( 𝐺 ↾ dom 𝐺 ) = 𝐺 )
35 33 34 syl ⊢ ( 𝜑 → ( 𝐺 ↾ dom 𝐺 ) = 𝐺 )
36 32 35 eqtrd ⊢ ( 𝜑 → 𝑌 = 𝐺 )
37 21 28 36 jca32 ⊢ ( 𝜑 → ( ( 𝑃 = 𝐴 ∧ 𝐸 = 𝐶 ) ∧ ( 𝑋 = 𝐹 ∧ 𝑌 = 𝐺 ) ) )