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 ( ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 ∧ 𝐸 ∈ 𝑉 ) → ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 ∧ 𝑃 = ( 𝐸 “ ran 𝐹 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) → ( ♯ ‘ 𝐹 ) = 𝑁 ) )

Proof

Step Hyp Ref Expression
1 fveqeq2 ⊢ ( 𝑃 = ( 𝐸 “ ran 𝐹 ) → ( ( ♯ ‘ 𝑃 ) = 𝑁 ↔ ( ♯ ‘ ( 𝐸 “ ran 𝐹 ) ) = 𝑁 ) )
2 1 adantl ⊢ ( ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 ∧ ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 ∧ 𝐸 ∈ 𝑉 ) ) ∧ 𝑃 = ( 𝐸 “ ran 𝐹 ) ) → ( ( ♯ ‘ 𝑃 ) = 𝑁 ↔ ( ♯ ‘ ( 𝐸 “ ran 𝐹 ) ) = 𝑁 ) )
3 hashimarn ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 ∧ 𝐸 ∈ 𝑉 ) → ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 → ( ♯ ‘ ( 𝐸 “ ran 𝐹 ) ) = ( ♯ ‘ 𝐹 ) ) )
4 3 impcom ⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 ∧ ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 ∧ 𝐸 ∈ 𝑉 ) ) → ( ♯ ‘ ( 𝐸 “ ran 𝐹 ) ) = ( ♯ ‘ 𝐹 ) )
5 id ⊢ ( ( ♯ ‘ ( 𝐸 “ ran 𝐹 ) ) = 𝑁 → ( ♯ ‘ ( 𝐸 “ ran 𝐹 ) ) = 𝑁 )
6 4 5 sylan9req ⊢ ( ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 ∧ ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 ∧ 𝐸 ∈ 𝑉 ) ) ∧ ( ♯ ‘ ( 𝐸 “ ran 𝐹 ) ) = 𝑁 ) → ( ♯ ‘ 𝐹 ) = 𝑁 )
7 6 ex ⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 ∧ ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 ∧ 𝐸 ∈ 𝑉 ) ) → ( ( ♯ ‘ ( 𝐸 “ ran 𝐹 ) ) = 𝑁 → ( ♯ ‘ 𝐹 ) = 𝑁 ) )
8 7 adantr ⊢ ( ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 ∧ ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 ∧ 𝐸 ∈ 𝑉 ) ) ∧ 𝑃 = ( 𝐸 “ ran 𝐹 ) ) → ( ( ♯ ‘ ( 𝐸 “ ran 𝐹 ) ) = 𝑁 → ( ♯ ‘ 𝐹 ) = 𝑁 ) )
9 2 8 sylbid ⊢ ( ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 ∧ ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 ∧ 𝐸 ∈ 𝑉 ) ) ∧ 𝑃 = ( 𝐸 “ ran 𝐹 ) ) → ( ( ♯ ‘ 𝑃 ) = 𝑁 → ( ♯ ‘ 𝐹 ) = 𝑁 ) )
10 9 exp31 ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 → ( ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 ∧ 𝐸 ∈ 𝑉 ) → ( 𝑃 = ( 𝐸 “ ran 𝐹 ) → ( ( ♯ ‘ 𝑃 ) = 𝑁 → ( ♯ ‘ 𝐹 ) = 𝑁 ) ) ) )
11 10 com23 ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 → ( 𝑃 = ( 𝐸 “ ran 𝐹 ) → ( ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 ∧ 𝐸 ∈ 𝑉 ) → ( ( ♯ ‘ 𝑃 ) = 𝑁 → ( ♯ ‘ 𝐹 ) = 𝑁 ) ) ) )
12 11 com34 ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 → ( 𝑃 = ( 𝐸 “ ran 𝐹 ) → ( ( ♯ ‘ 𝑃 ) = 𝑁 → ( ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 ∧ 𝐸 ∈ 𝑉 ) → ( ♯ ‘ 𝐹 ) = 𝑁 ) ) ) )
13 12 3imp ⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 ∧ 𝑃 = ( 𝐸 “ ran 𝐹 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) → ( ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 ∧ 𝐸 ∈ 𝑉 ) → ( ♯ ‘ 𝐹 ) = 𝑁 ) )
14 13 com12 ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 ∧ 𝐸 ∈ 𝑉 ) → ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 ∧ 𝑃 = ( 𝐸 “ ran 𝐹 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) → ( ♯ ‘ 𝐹 ) = 𝑁 ) )