Metamath Proof Explorer

Theorem fcoreslem2

Description: Lemma 2 for fcores . (Contributed by AV, 17-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 )
Assertion fcoreslem2 
|- ( ph -> ran X = E )

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 df-ima 
 |-  ( F " P ) = ran ( F |` P )
6 4 rneqi 
 |-  ran X = ran ( F |` P )
7 6 eqcomi 
 |-  ran ( F |` P ) = ran X
8 7 a1i 
 |-  ( ph -> ran ( F |` P ) = ran X )
9 5 8 eqtr2id 
 |-  ( ph -> ran X = ( F " P ) )
10 1 2 3 fcoreslem1 
 |-  ( ph -> P = ( `' F " E ) )
11 10 imaeq2d 
 |-  ( ph -> ( F " P ) = ( F " ( `' F " E ) ) )
12 1 ffund 
 |-  ( ph -> Fun F )
13 funimacnv 
 |-  ( Fun F -> ( F " ( `' F " E ) ) = ( E i^i ran F ) )
14 12 13 syl 
 |-  ( ph -> ( F " ( `' F " E ) ) = ( E i^i ran F ) )
15 inss1 
 |-  ( ran F i^i C ) C_ ran F
16 2 15 eqsstri 
 |-  E C_ ran F
17 16 a1i 
 |-  ( ph -> E C_ ran F )
18 df-ss 
 |-  ( E C_ ran F <-> ( E i^i ran F ) = E )
19 17 18 sylib 
 |-  ( ph -> ( E i^i ran F ) = E )
20 14 19 eqtrd 
 |-  ( ph -> ( F " ( `' F " E ) ) = E )
21 9 11 20 3eqtrd 
 |-  ( ph -> ran X = E )