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 df-ima ⊢ E ran ⁡ F = ran ⁡ E ↾ ran ⁡ F
8 7 fveq2i ⊢ E ran ⁡ F = ran ⁡ E ↾ ran ⁡ F
9 f1fun ⊢ E : dom ⁡ E ⟶ 1-1 ran ⁡ E → Fun ⁡ E
10 funres ⊢ Fun ⁡ E → Fun ⁡ E ↾ ran ⁡ F
11 10 funfnd ⊢ Fun ⁡ E → E ↾ ran ⁡ F Fn dom ⁡ E ↾ ran ⁡ F
12 9 11 syl ⊢ E : dom ⁡ E ⟶ 1-1 ran ⁡ E → E ↾ ran ⁡ F Fn dom ⁡ E ↾ ran ⁡ F
13 12 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
14 hashfn ⊢ E ↾ ran ⁡ F Fn dom ⁡ E ↾ ran ⁡ F → E ↾ ran ⁡ F = dom ⁡ E ↾ ran ⁡ F
15 13 14 syl ⊢ E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ E ∈ V ∧ F : 0 ..^ F ⟶ 1-1 dom ⁡ E → E ↾ ran ⁡ F = dom ⁡ E ↾ ran ⁡ F
16 ovex ⊢ 0 ..^ F ∈ V
17 fex ⊢ F : 0 ..^ F ⟶ dom ⁡ E ∧ 0 ..^ F ∈ V → F ∈ V
18 1 16 17 sylancl ⊢ F : 0 ..^ F ⟶ 1-1 dom ⁡ E → F ∈ V
19 rnexg ⊢ F ∈ V → ran ⁡ F ∈ V
20 18 19 syl ⊢ F : 0 ..^ F ⟶ 1-1 dom ⁡ E → ran ⁡ F ∈ V
21 simpll ⊢ E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ E ∈ V ∧ F : 0 ..^ F ⟶ 1-1 dom ⁡ E → E : dom ⁡ E ⟶ 1-1 ran ⁡ E
22 f1ssres ⊢ E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ ran ⁡ F ⊆ dom ⁡ E → E ↾ ran ⁡ F : ran ⁡ F ⟶ 1-1 ran ⁡ E
23 21 3 22 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
24 hashf1rn ⊢ ran ⁡ F ∈ V ∧ E ↾ ran ⁡ F : ran ⁡ F ⟶ 1-1 ran ⁡ E → E ↾ ran ⁡ F = ran ⁡ E ↾ ran ⁡ F
25 20 23 24 syl2an2 ⊢ E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ E ∈ V ∧ F : 0 ..^ F ⟶ 1-1 dom ⁡ E → E ↾ ran ⁡ F = ran ⁡ E ↾ ran ⁡ F
26 15 25 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
27 8 26 eqtr4id ⊢ 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 16 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