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