Metamath Proof Explorer


Theorem f1dmvrnfibi

Description: A one-to-one function whose domain is a set is finite if and only if its range is finite. See also f1vrnfibi . (Contributed by AV, 10-Jan-2020)

Ref Expression
Assertion f1dmvrnfibi ( ( 𝐴𝑉𝐹 : 𝐴1-1𝐵 ) → ( 𝐹 ∈ Fin ↔ ran 𝐹 ∈ Fin ) )

Proof

Step Hyp Ref Expression
1 rnfi ( 𝐹 ∈ Fin → ran 𝐹 ∈ Fin )
2 simpr ( ( ( 𝐴𝑉𝐹 : 𝐴1-1𝐵 ) ∧ ran 𝐹 ∈ Fin ) → ran 𝐹 ∈ Fin )
3 f1dm ( 𝐹 : 𝐴1-1𝐵 → dom 𝐹 = 𝐴 )
4 f1f1orn ( 𝐹 : 𝐴1-1𝐵𝐹 : 𝐴1-1-onto→ ran 𝐹 )
5 eleq1 ( 𝐴 = dom 𝐹 → ( 𝐴𝑉 ↔ dom 𝐹𝑉 ) )
6 f1oeq2 ( 𝐴 = dom 𝐹 → ( 𝐹 : 𝐴1-1-onto→ ran 𝐹𝐹 : dom 𝐹1-1-onto→ ran 𝐹 ) )
7 5 6 anbi12d ( 𝐴 = dom 𝐹 → ( ( 𝐴𝑉𝐹 : 𝐴1-1-onto→ ran 𝐹 ) ↔ ( dom 𝐹𝑉𝐹 : dom 𝐹1-1-onto→ ran 𝐹 ) ) )
8 7 eqcoms ( dom 𝐹 = 𝐴 → ( ( 𝐴𝑉𝐹 : 𝐴1-1-onto→ ran 𝐹 ) ↔ ( dom 𝐹𝑉𝐹 : dom 𝐹1-1-onto→ ran 𝐹 ) ) )
9 8 biimpd ( dom 𝐹 = 𝐴 → ( ( 𝐴𝑉𝐹 : 𝐴1-1-onto→ ran 𝐹 ) → ( dom 𝐹𝑉𝐹 : dom 𝐹1-1-onto→ ran 𝐹 ) ) )
10 9 expcomd ( dom 𝐹 = 𝐴 → ( 𝐹 : 𝐴1-1-onto→ ran 𝐹 → ( 𝐴𝑉 → ( dom 𝐹𝑉𝐹 : dom 𝐹1-1-onto→ ran 𝐹 ) ) ) )
11 3 4 10 sylc ( 𝐹 : 𝐴1-1𝐵 → ( 𝐴𝑉 → ( dom 𝐹𝑉𝐹 : dom 𝐹1-1-onto→ ran 𝐹 ) ) )
12 11 impcom ( ( 𝐴𝑉𝐹 : 𝐴1-1𝐵 ) → ( dom 𝐹𝑉𝐹 : dom 𝐹1-1-onto→ ran 𝐹 ) )
13 12 adantr ( ( ( 𝐴𝑉𝐹 : 𝐴1-1𝐵 ) ∧ ran 𝐹 ∈ Fin ) → ( dom 𝐹𝑉𝐹 : dom 𝐹1-1-onto→ ran 𝐹 ) )
14 f1oeng ( ( dom 𝐹𝑉𝐹 : dom 𝐹1-1-onto→ ran 𝐹 ) → dom 𝐹 ≈ ran 𝐹 )
15 13 14 syl ( ( ( 𝐴𝑉𝐹 : 𝐴1-1𝐵 ) ∧ ran 𝐹 ∈ Fin ) → dom 𝐹 ≈ ran 𝐹 )
16 enfii ( ( ran 𝐹 ∈ Fin ∧ dom 𝐹 ≈ ran 𝐹 ) → dom 𝐹 ∈ Fin )
17 2 15 16 syl2anc ( ( ( 𝐴𝑉𝐹 : 𝐴1-1𝐵 ) ∧ ran 𝐹 ∈ Fin ) → dom 𝐹 ∈ Fin )
18 f1fun ( 𝐹 : 𝐴1-1𝐵 → Fun 𝐹 )
19 18 ad2antlr ( ( ( 𝐴𝑉𝐹 : 𝐴1-1𝐵 ) ∧ ran 𝐹 ∈ Fin ) → Fun 𝐹 )
20 fundmfibi ( Fun 𝐹 → ( 𝐹 ∈ Fin ↔ dom 𝐹 ∈ Fin ) )
21 19 20 syl ( ( ( 𝐴𝑉𝐹 : 𝐴1-1𝐵 ) ∧ ran 𝐹 ∈ Fin ) → ( 𝐹 ∈ Fin ↔ dom 𝐹 ∈ Fin ) )
22 17 21 mpbird ( ( ( 𝐴𝑉𝐹 : 𝐴1-1𝐵 ) ∧ ran 𝐹 ∈ Fin ) → 𝐹 ∈ Fin )
23 22 ex ( ( 𝐴𝑉𝐹 : 𝐴1-1𝐵 ) → ( ran 𝐹 ∈ Fin → 𝐹 ∈ Fin ) )
24 1 23 impbid2 ( ( 𝐴𝑉𝐹 : 𝐴1-1𝐵 ) → ( 𝐹 ∈ Fin ↔ ran 𝐹 ∈ Fin ) )