Metamath Proof Explorer

Theorem hashimarn

Description: The size of the image of a one-to-one function E under the range of a function F which is a one-to-one function into the domain of E equals the size of the function F . (Contributed by Alexander van der Vekens, 4-Feb-2018) (Proof shortened by AV, 4-May-2021)

Ref Expression
Assertion hashimarn ⊢ E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ E ∈ V → F : 0 ..^ F ⟶ 1-1 dom ⁡ E → E ran ⁡ F = F

Proof

Step Hyp Ref Expression
1 f1f ⊢ F : 0 ..^ F ⟶ 1-1 dom ⁡ E → F : 0 ..^ F ⟶ dom ⁡ E
2 1 frnd ⊢ F : 0 ..^ F ⟶ 1-1 dom ⁡ E → ran ⁡ F ⊆ dom ⁡ E
3 2 adantl ⊢ E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ E ∈ V ∧ F : 0 ..^ F ⟶ 1-1 dom ⁡ E → ran ⁡ F ⊆ dom ⁡ E
4 ssdmres ⊢ ran ⁡ F ⊆ dom ⁡ E ↔ dom ⁡ E ↾ ran ⁡ F = ran ⁡ F
5 3 4 sylib ⊢ E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ E ∈ V ∧ F : 0 ..^ F ⟶ 1-1 dom ⁡ E → dom ⁡ E ↾ ran ⁡ F = ran ⁡ F
6 5 fveq2d ⊢ E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ E ∈ V ∧ F : 0 ..^ F ⟶ 1-1 dom ⁡ E → dom ⁡ E ↾ ran ⁡ F = ran ⁡ F
7 f1fun ⊢ E : dom ⁡ E ⟶ 1-1 ran ⁡ E → Fun ⁡ E
8 funres ⊢ Fun ⁡ E → Fun ⁡ E ↾ ran ⁡ F
9 8 funfnd ⊢ Fun ⁡ E → E ↾ ran ⁡ F Fn dom ⁡ E ↾ ran ⁡ F
10 7 9 syl ⊢ E : dom ⁡ E ⟶ 1-1 ran ⁡ E → E ↾ ran ⁡ F Fn dom ⁡ E ↾ ran ⁡ F
11 10 ad2antrr ⊢ E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ E ∈ V ∧ F : 0 ..^ F ⟶ 1-1 dom ⁡ E → E ↾ ran ⁡ F Fn dom ⁡ E ↾ ran ⁡ F
12 hashfn ⊢ E ↾ ran ⁡ F Fn dom ⁡ E ↾ ran ⁡ F → E ↾ ran ⁡ F = dom ⁡ E ↾ ran ⁡ F
13 11 12 syl ⊢ E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ E ∈ V ∧ F : 0 ..^ F ⟶ 1-1 dom ⁡ E → E ↾ ran ⁡ F = dom ⁡ E ↾ ran ⁡ F
14 ovex ⊢ 0 ..^ F ∈ V
15 fex ⊢ F : 0 ..^ F ⟶ dom ⁡ E ∧ 0 ..^ F ∈ V → F ∈ V
16 1 14 15 sylancl ⊢ F : 0 ..^ F ⟶ 1-1 dom ⁡ E → F ∈ V
17 rnexg ⊢ F ∈ V → ran ⁡ F ∈ V
18 16 17 syl ⊢ F : 0 ..^ F ⟶ 1-1 dom ⁡ E → ran ⁡ F ∈ V
19 simpll ⊢ E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ E ∈ V ∧ F : 0 ..^ F ⟶ 1-1 dom ⁡ E → E : dom ⁡ E ⟶ 1-1 ran ⁡ E
20 f1ssres ⊢ E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ ran ⁡ F ⊆ dom ⁡ E → E ↾ ran ⁡ F : ran ⁡ F ⟶ 1-1 ran ⁡ E
21 19 3 20 syl2anc ⊢ E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ E ∈ V ∧ F : 0 ..^ F ⟶ 1-1 dom ⁡ E → E ↾ ran ⁡ F : ran ⁡ F ⟶ 1-1 ran ⁡ E
22 hashf1rn ⊢ ran ⁡ F ∈ V ∧ E ↾ ran ⁡ F : ran ⁡ F ⟶ 1-1 ran ⁡ E → E ↾ ran ⁡ F = ran ⁡ E ↾ ran ⁡ F
23 18 21 22 syl2an2 ⊢ E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ E ∈ V ∧ F : 0 ..^ F ⟶ 1-1 dom ⁡ E → E ↾ ran ⁡ F = ran ⁡ E ↾ ran ⁡ F
24 13 23 eqtr3d ⊢ E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ E ∈ V ∧ F : 0 ..^ F ⟶ 1-1 dom ⁡ E → dom ⁡ E ↾ ran ⁡ F = ran ⁡ E ↾ ran ⁡ F
25 df-ima ⊢ E ran ⁡ F = ran ⁡ E ↾ ran ⁡ F
26 25 fveq2i ⊢ E ran ⁡ F = ran ⁡ E ↾ ran ⁡ F
27 24 26 syl6reqr ⊢ E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ E ∈ V ∧ F : 0 ..^ F ⟶ 1-1 dom ⁡ E → E ran ⁡ F = dom ⁡ E ↾ ran ⁡ F
28 hashf1rn ⊢ 0 ..^ F ∈ V ∧ F : 0 ..^ F ⟶ 1-1 dom ⁡ E → F = ran ⁡ F
29 14 28 mpan ⊢ F : 0 ..^ F ⟶ 1-1 dom ⁡ E → F = ran ⁡ F
30 29 adantl ⊢ E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ E ∈ V ∧ F : 0 ..^ F ⟶ 1-1 dom ⁡ E → F = ran ⁡ F
31 6 27 30 3eqtr4d ⊢ E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ E ∈ V ∧ F : 0 ..^ F ⟶ 1-1 dom ⁡ E → E ran ⁡ F = F
32 31 ex ⊢ E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ E ∈ V → F : 0 ..^ F ⟶ 1-1 dom ⁡ E → E ran ⁡ F = F