Metamath Proof Explorer


Theorem f1finf1o

Description: Any injection from one finite set to another of equal size must be a bijection. (Contributed by Jeff Madsen, 5-Jun-2010) (Revised by Mario Carneiro, 27-Feb-2014) Avoid ax-pow . (Revised by BTernaryTau, 4-Jan-2025)

Ref Expression
Assertion f1finf1o ( ( 𝐴𝐵𝐵 ∈ Fin ) → ( 𝐹 : 𝐴1-1𝐵𝐹 : 𝐴1-1-onto𝐵 ) )

Proof

Step Hyp Ref Expression
1 simpr ( ( ( 𝐴𝐵𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴1-1𝐵 ) → 𝐹 : 𝐴1-1𝐵 )
2 f1f ( 𝐹 : 𝐴1-1𝐵𝐹 : 𝐴𝐵 )
3 2 adantl ( ( ( 𝐴𝐵𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴1-1𝐵 ) → 𝐹 : 𝐴𝐵 )
4 3 ffnd ( ( ( 𝐴𝐵𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴1-1𝐵 ) → 𝐹 Fn 𝐴 )
5 simpll ( ( ( 𝐴𝐵𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴1-1𝐵 ) → 𝐴𝐵 )
6 3 frnd ( ( ( 𝐴𝐵𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴1-1𝐵 ) → ran 𝐹𝐵 )
7 df-pss ( ran 𝐹𝐵 ↔ ( ran 𝐹𝐵 ∧ ran 𝐹𝐵 ) )
8 7 baib ( ran 𝐹𝐵 → ( ran 𝐹𝐵 ↔ ran 𝐹𝐵 ) )
9 6 8 syl ( ( ( 𝐴𝐵𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴1-1𝐵 ) → ( ran 𝐹𝐵 ↔ ran 𝐹𝐵 ) )
10 php3 ( ( 𝐵 ∈ Fin ∧ ran 𝐹𝐵 ) → ran 𝐹𝐵 )
11 10 ex ( 𝐵 ∈ Fin → ( ran 𝐹𝐵 → ran 𝐹𝐵 ) )
12 11 ad2antlr ( ( ( 𝐴𝐵𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴1-1𝐵 ) → ( ran 𝐹𝐵 → ran 𝐹𝐵 ) )
13 enfii ( ( 𝐵 ∈ Fin ∧ 𝐴𝐵 ) → 𝐴 ∈ Fin )
14 13 ancoms ( ( 𝐴𝐵𝐵 ∈ Fin ) → 𝐴 ∈ Fin )
15 f1f1orn ( 𝐹 : 𝐴1-1𝐵𝐹 : 𝐴1-1-onto→ ran 𝐹 )
16 f1oenfi ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴1-1-onto→ ran 𝐹 ) → 𝐴 ≈ ran 𝐹 )
17 14 15 16 syl2an ( ( ( 𝐴𝐵𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴1-1𝐵 ) → 𝐴 ≈ ran 𝐹 )
18 endom ( 𝐴 ≈ ran 𝐹𝐴 ≼ ran 𝐹 )
19 domsdomtrfi ( ( 𝐴 ∈ Fin ∧ 𝐴 ≼ ran 𝐹 ∧ ran 𝐹𝐵 ) → 𝐴𝐵 )
20 18 19 syl3an2 ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ ran 𝐹 ∧ ran 𝐹𝐵 ) → 𝐴𝐵 )
21 20 3expia ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ ran 𝐹 ) → ( ran 𝐹𝐵𝐴𝐵 ) )
22 14 17 21 syl2an2r ( ( ( 𝐴𝐵𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴1-1𝐵 ) → ( ran 𝐹𝐵𝐴𝐵 ) )
23 12 22 syld ( ( ( 𝐴𝐵𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴1-1𝐵 ) → ( ran 𝐹𝐵𝐴𝐵 ) )
24 sdomnen ( 𝐴𝐵 → ¬ 𝐴𝐵 )
25 23 24 syl6 ( ( ( 𝐴𝐵𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴1-1𝐵 ) → ( ran 𝐹𝐵 → ¬ 𝐴𝐵 ) )
26 9 25 sylbird ( ( ( 𝐴𝐵𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴1-1𝐵 ) → ( ran 𝐹𝐵 → ¬ 𝐴𝐵 ) )
27 26 necon4ad ( ( ( 𝐴𝐵𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴1-1𝐵 ) → ( 𝐴𝐵 → ran 𝐹 = 𝐵 ) )
28 5 27 mpd ( ( ( 𝐴𝐵𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴1-1𝐵 ) → ran 𝐹 = 𝐵 )
29 df-fo ( 𝐹 : 𝐴onto𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵 ) )
30 4 28 29 sylanbrc ( ( ( 𝐴𝐵𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴1-1𝐵 ) → 𝐹 : 𝐴onto𝐵 )
31 df-f1o ( 𝐹 : 𝐴1-1-onto𝐵 ↔ ( 𝐹 : 𝐴1-1𝐵𝐹 : 𝐴onto𝐵 ) )
32 1 30 31 sylanbrc ( ( ( 𝐴𝐵𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴1-1𝐵 ) → 𝐹 : 𝐴1-1-onto𝐵 )
33 32 ex ( ( 𝐴𝐵𝐵 ∈ Fin ) → ( 𝐹 : 𝐴1-1𝐵𝐹 : 𝐴1-1-onto𝐵 ) )
34 f1of1 ( 𝐹 : 𝐴1-1-onto𝐵𝐹 : 𝐴1-1𝐵 )
35 33 34 impbid1 ( ( 𝐴𝐵𝐵 ∈ Fin ) → ( 𝐹 : 𝐴1-1𝐵𝐹 : 𝐴1-1-onto𝐵 ) )