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)

	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		simplr	⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐵 ∈ Fin )
11		relen	⊢ Rel ≈
12	11	brrelex1i	⊢ ( 𝐴 ≈ 𝐵 → 𝐴 ∈ V )
13	5 12	syl	⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐴 ∈ V )
14	10 13	elmapd	⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ↔ 𝐹 : 𝐴 ⟶ 𝐵 ) )
15	3 14	mpbird	⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) )
16		f1f1orn	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 )
17	16	adantl	⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 )
18		f1oen3g	⊢ ( ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 ) → 𝐴 ≈ ran 𝐹 )
19	15 17 18	syl2anc	⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐴 ≈ ran 𝐹 )
20		php3	⊢ ( ( 𝐵 ∈ Fin ∧ ran 𝐹 ⊊ 𝐵 ) → ran 𝐹 ≺ 𝐵 )
21	20	ex	⊢ ( 𝐵 ∈ Fin → ( ran 𝐹 ⊊ 𝐵 → ran 𝐹 ≺ 𝐵 ) )
22	10 21	syl	⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( ran 𝐹 ⊊ 𝐵 → ran 𝐹 ≺ 𝐵 ) )
23		ensdomtr	⊢ ( ( 𝐴 ≈ ran 𝐹 ∧ ran 𝐹 ≺ 𝐵 ) → 𝐴 ≺ 𝐵 )
24	19 22 23	syl6an	⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( ran 𝐹 ⊊ 𝐵 → 𝐴 ≺ 𝐵 ) )
25		sdomnen	⊢ ( 𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵 )
26	24 25	syl6	⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( ran 𝐹 ⊊ 𝐵 → ¬ 𝐴 ≈ 𝐵 ) )
27	9 26	sylbird	⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( ran 𝐹 ≠ 𝐵 → ¬ 𝐴 ≈ 𝐵 ) )
28	27	necon4ad	⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( 𝐴 ≈ 𝐵 → ran 𝐹 = 𝐵 ) )
29	5 28	mpd	⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ran 𝐹 = 𝐵 )
30		df-fo	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵 ) )
31	4 29 30	sylanbrc	⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐹 : 𝐴 –onto→ 𝐵 )
32		df-f1o	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) )
33	1 31 32	sylanbrc	⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
34	33	ex	⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) )
35		f1of1	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 : 𝐴 –1-1→ 𝐵 )
36	34 35	impbid1	⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) )