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

Metamath Proof Explorer

Theorem fcoreslem2

Description: Lemma 2 for fcores . (Contributed by AV, 17-Sep-2024)

Ref Expression
Hypotheses fcores.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
fcores.e ⊢ 𝐸 = ( ran 𝐹 ∩ 𝐶 )
fcores.p ⊢ 𝑃 = ( ◡ 𝐹 “ 𝐶 )
fcores.x ⊢ 𝑋 = ( 𝐹 ↾ 𝑃 )
Assertion fcoreslem2 ( 𝜑 → ran 𝑋 = 𝐸 )

Proof

Step Hyp Ref Expression
1 fcores.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2 fcores.e ⊢ 𝐸 = ( ran 𝐹 ∩ 𝐶 )
3 fcores.p ⊢ 𝑃 = ( ◡ 𝐹 “ 𝐶 )
4 fcores.x ⊢ 𝑋 = ( 𝐹 ↾ 𝑃 )
5 df-ima ⊢ ( 𝐹 “ 𝑃 ) = ran ( 𝐹 ↾ 𝑃 )
6 4 rneqi ⊢ ran 𝑋 = ran ( 𝐹 ↾ 𝑃 )
7 6 eqcomi ⊢ ran ( 𝐹 ↾ 𝑃 ) = ran 𝑋
8 7 a1i ⊢ ( 𝜑 → ran ( 𝐹 ↾ 𝑃 ) = ran 𝑋 )
9 5 8 eqtr2id ⊢ ( 𝜑 → ran 𝑋 = ( 𝐹 “ 𝑃 ) )
10 1 2 3 fcoreslem1 ⊢ ( 𝜑 → 𝑃 = ( ◡ 𝐹 “ 𝐸 ) )
11 10 imaeq2d ⊢ ( 𝜑 → ( 𝐹 “ 𝑃 ) = ( 𝐹 “ ( ◡ 𝐹 “ 𝐸 ) ) )
12 1 ffund ⊢ ( 𝜑 → Fun 𝐹 )
13 funimacnv ⊢ ( Fun 𝐹 → ( 𝐹 “ ( ◡ 𝐹 “ 𝐸 ) ) = ( 𝐸 ∩ ran 𝐹 ) )
14 12 13 syl ⊢ ( 𝜑 → ( 𝐹 “ ( ◡ 𝐹 “ 𝐸 ) ) = ( 𝐸 ∩ ran 𝐹 ) )
15 inss1 ⊢ ( ran 𝐹 ∩ 𝐶 ) ⊆ ran 𝐹
16 2 15 eqsstri ⊢ 𝐸 ⊆ ran 𝐹
17 16 a1i ⊢ ( 𝜑 → 𝐸 ⊆ ran 𝐹 )
18 dfss2 ⊢ ( 𝐸 ⊆ ran 𝐹 ↔ ( 𝐸 ∩ ran 𝐹 ) = 𝐸 )
19 17 18 sylib ⊢ ( 𝜑 → ( 𝐸 ∩ ran 𝐹 ) = 𝐸 )
20 14 19 eqtrd ⊢ ( 𝜑 → ( 𝐹 “ ( ◡ 𝐹 “ 𝐸 ) ) = 𝐸 )
21 9 11 20 3eqtrd ⊢ ( 𝜑 → ran 𝑋 = 𝐸 )