# 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 ${⊢}\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}\mathrm{ran}{E}\wedge {E}\in {V}\right)\to \left({F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}{E}\to \left|{E}\left[\mathrm{ran}{F}\right]\right|=\left|{F}\right|\right)$

### Proof

Step Hyp Ref Expression
1 f1f ${⊢}{F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}{E}\to {F}:\left(0..^\left|{F}\right|\right)⟶\mathrm{dom}{E}$
2 1 frnd ${⊢}{F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}{E}\to \mathrm{ran}{F}\subseteq \mathrm{dom}{E}$
3 2 adantl ${⊢}\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}\mathrm{ran}{E}\wedge {E}\in {V}\right)\wedge {F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}{E}\right)\to \mathrm{ran}{F}\subseteq \mathrm{dom}{E}$
4 ssdmres ${⊢}\mathrm{ran}{F}\subseteq \mathrm{dom}{E}↔\mathrm{dom}\left({{E}↾}_{\mathrm{ran}{F}}\right)=\mathrm{ran}{F}$
5 3 4 sylib ${⊢}\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}\mathrm{ran}{E}\wedge {E}\in {V}\right)\wedge {F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}{E}\right)\to \mathrm{dom}\left({{E}↾}_{\mathrm{ran}{F}}\right)=\mathrm{ran}{F}$
6 5 fveq2d ${⊢}\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}\mathrm{ran}{E}\wedge {E}\in {V}\right)\wedge {F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}{E}\right)\to \left|\mathrm{dom}\left({{E}↾}_{\mathrm{ran}{F}}\right)\right|=\left|\mathrm{ran}{F}\right|$
7 f1fun ${⊢}{E}:\mathrm{dom}{E}\underset{1-1}{⟶}\mathrm{ran}{E}\to \mathrm{Fun}{E}$
8 funres ${⊢}\mathrm{Fun}{E}\to \mathrm{Fun}\left({{E}↾}_{\mathrm{ran}{F}}\right)$
9 8 funfnd ${⊢}\mathrm{Fun}{E}\to \left({{E}↾}_{\mathrm{ran}{F}}\right)Fn\mathrm{dom}\left({{E}↾}_{\mathrm{ran}{F}}\right)$
10 7 9 syl ${⊢}{E}:\mathrm{dom}{E}\underset{1-1}{⟶}\mathrm{ran}{E}\to \left({{E}↾}_{\mathrm{ran}{F}}\right)Fn\mathrm{dom}\left({{E}↾}_{\mathrm{ran}{F}}\right)$
11 10 ad2antrr ${⊢}\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}\mathrm{ran}{E}\wedge {E}\in {V}\right)\wedge {F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}{E}\right)\to \left({{E}↾}_{\mathrm{ran}{F}}\right)Fn\mathrm{dom}\left({{E}↾}_{\mathrm{ran}{F}}\right)$
12 hashfn ${⊢}\left({{E}↾}_{\mathrm{ran}{F}}\right)Fn\mathrm{dom}\left({{E}↾}_{\mathrm{ran}{F}}\right)\to \left|{{E}↾}_{\mathrm{ran}{F}}\right|=\left|\mathrm{dom}\left({{E}↾}_{\mathrm{ran}{F}}\right)\right|$
13 11 12 syl ${⊢}\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}\mathrm{ran}{E}\wedge {E}\in {V}\right)\wedge {F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}{E}\right)\to \left|{{E}↾}_{\mathrm{ran}{F}}\right|=\left|\mathrm{dom}\left({{E}↾}_{\mathrm{ran}{F}}\right)\right|$
14 ovex ${⊢}\left(0..^\left|{F}\right|\right)\in \mathrm{V}$
15 fex ${⊢}\left({F}:\left(0..^\left|{F}\right|\right)⟶\mathrm{dom}{E}\wedge \left(0..^\left|{F}\right|\right)\in \mathrm{V}\right)\to {F}\in \mathrm{V}$
16 1 14 15 sylancl ${⊢}{F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}{E}\to {F}\in \mathrm{V}$
17 rnexg ${⊢}{F}\in \mathrm{V}\to \mathrm{ran}{F}\in \mathrm{V}$
18 16 17 syl ${⊢}{F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}{E}\to \mathrm{ran}{F}\in \mathrm{V}$
19 simpll ${⊢}\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}\mathrm{ran}{E}\wedge {E}\in {V}\right)\wedge {F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}{E}\right)\to {E}:\mathrm{dom}{E}\underset{1-1}{⟶}\mathrm{ran}{E}$
20 f1ssres ${⊢}\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}\mathrm{ran}{E}\wedge \mathrm{ran}{F}\subseteq \mathrm{dom}{E}\right)\to \left({{E}↾}_{\mathrm{ran}{F}}\right):\mathrm{ran}{F}\underset{1-1}{⟶}\mathrm{ran}{E}$
21 19 3 20 syl2anc ${⊢}\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}\mathrm{ran}{E}\wedge {E}\in {V}\right)\wedge {F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}{E}\right)\to \left({{E}↾}_{\mathrm{ran}{F}}\right):\mathrm{ran}{F}\underset{1-1}{⟶}\mathrm{ran}{E}$
22 hashf1rn ${⊢}\left(\mathrm{ran}{F}\in \mathrm{V}\wedge \left({{E}↾}_{\mathrm{ran}{F}}\right):\mathrm{ran}{F}\underset{1-1}{⟶}\mathrm{ran}{E}\right)\to \left|{{E}↾}_{\mathrm{ran}{F}}\right|=\left|\mathrm{ran}\left({{E}↾}_{\mathrm{ran}{F}}\right)\right|$
23 18 21 22 syl2an2 ${⊢}\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}\mathrm{ran}{E}\wedge {E}\in {V}\right)\wedge {F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}{E}\right)\to \left|{{E}↾}_{\mathrm{ran}{F}}\right|=\left|\mathrm{ran}\left({{E}↾}_{\mathrm{ran}{F}}\right)\right|$
24 13 23 eqtr3d ${⊢}\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}\mathrm{ran}{E}\wedge {E}\in {V}\right)\wedge {F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}{E}\right)\to \left|\mathrm{dom}\left({{E}↾}_{\mathrm{ran}{F}}\right)\right|=\left|\mathrm{ran}\left({{E}↾}_{\mathrm{ran}{F}}\right)\right|$
25 df-ima ${⊢}{E}\left[\mathrm{ran}{F}\right]=\mathrm{ran}\left({{E}↾}_{\mathrm{ran}{F}}\right)$
26 25 fveq2i ${⊢}\left|{E}\left[\mathrm{ran}{F}\right]\right|=\left|\mathrm{ran}\left({{E}↾}_{\mathrm{ran}{F}}\right)\right|$
27 24 26 syl6reqr ${⊢}\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}\mathrm{ran}{E}\wedge {E}\in {V}\right)\wedge {F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}{E}\right)\to \left|{E}\left[\mathrm{ran}{F}\right]\right|=\left|\mathrm{dom}\left({{E}↾}_{\mathrm{ran}{F}}\right)\right|$
28 hashf1rn ${⊢}\left(\left(0..^\left|{F}\right|\right)\in \mathrm{V}\wedge {F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}{E}\right)\to \left|{F}\right|=\left|\mathrm{ran}{F}\right|$
29 14 28 mpan ${⊢}{F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}{E}\to \left|{F}\right|=\left|\mathrm{ran}{F}\right|$
30 29 adantl ${⊢}\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}\mathrm{ran}{E}\wedge {E}\in {V}\right)\wedge {F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}{E}\right)\to \left|{F}\right|=\left|\mathrm{ran}{F}\right|$
31 6 27 30 3eqtr4d ${⊢}\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}\mathrm{ran}{E}\wedge {E}\in {V}\right)\wedge {F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}{E}\right)\to \left|{E}\left[\mathrm{ran}{F}\right]\right|=\left|{F}\right|$
32 31 ex ${⊢}\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}\mathrm{ran}{E}\wedge {E}\in {V}\right)\to \left({F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}{E}\to \left|{E}\left[\mathrm{ran}{F}\right]\right|=\left|{F}\right|\right)$