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 ) )