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-1ran⁡E∧E∈V→F:0..^F⟶1-1dom⁡E∧P=Eran⁡F∧P=N→F=N

Proof

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