Metamath Proof Explorer

Theorem hashimarni

Description: If 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 is a nonnegative integer, the size of the function F is the same nonnegative integer. (Contributed by Alexander van der Vekens, 4-Feb-2018)

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

Proof

Step Hyp Ref Expression
1 fveqeq2 ⊢ P = E ran ⁡ F → P = N ↔ E ran ⁡ F = N
2 1 adantl ⊢ F : 0 ..^ F ⟶ 1-1 dom ⁡ E ∧ E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ E ∈ V ∧ P = E ran ⁡ F → P = N ↔ E ran ⁡ F = N
3 hashimarn ⊢ E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ E ∈ V → F : 0 ..^ F ⟶ 1-1 dom ⁡ E → E ran ⁡ F = F
4 3 impcom ⊢ F : 0 ..^ F ⟶ 1-1 dom ⁡ E ∧ E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ E ∈ V → E ran ⁡ F = F
5 id ⊢ E ran ⁡ F = N → E ran ⁡ F = N
6 4 5 sylan9req ⊢ F : 0 ..^ F ⟶ 1-1 dom ⁡ E ∧ E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ E ∈ V ∧ E ran ⁡ F = N → F = N
7 6 ex ⊢ F : 0 ..^ F ⟶ 1-1 dom ⁡ E ∧ E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ E ∈ V → E ran ⁡ F = N → F = N
8 7 adantr ⊢ F : 0 ..^ F ⟶ 1-1 dom ⁡ E ∧ E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ E ∈ V ∧ P = E ran ⁡ F → E ran ⁡ F = N → F = N
9 2 8 sylbid ⊢ F : 0 ..^ F ⟶ 1-1 dom ⁡ E ∧ E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ E ∈ V ∧ P = E ran ⁡ F → P = N → F = N
10 9 exp31 ⊢ F : 0 ..^ F ⟶ 1-1 dom ⁡ E → E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ E ∈ V → P = E ran ⁡ F → P = N → F = N
11 10 com23 ⊢ F : 0 ..^ F ⟶ 1-1 dom ⁡ E → P = E ran ⁡ F → E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ E ∈ V → P = N → F = N
12 11 com34 ⊢ F : 0 ..^ F ⟶ 1-1 dom ⁡ E → P = E ran ⁡ F → P = N → E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ E ∈ V → F = N
13 12 3imp ⊢ F : 0 ..^ F ⟶ 1-1 dom ⁡ E ∧ P = E ran ⁡ F ∧ P = N → E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ E ∈ V → F = N
14 13 com12 ⊢ E : dom ⁡ E ⟶ 1-1 ran ⁡ E ∧ E ∈ V → F : 0 ..^ F ⟶ 1-1 dom ⁡ E ∧ P = E ran ⁡ F ∧ P = N → F = N