Metamath Proof Explorer

Theorem fofinf1o

Description: Any surjection from one finite set to another of equal size must be a bijection. (Contributed by Mario Carneiro, 19-Aug-2014)

Ref Expression
Assertion fofinf1o ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → 𝐹 : 𝐴 –onto→ 𝐵 )
2 fof ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
3 1 2 syl ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → 𝐹 : 𝐴 ⟶ 𝐵 )
4 domnsym ⊢ ( 𝐵 ≼ ( 𝐴 ∖ { 𝑦 } ) → ¬ ( 𝐴 ∖ { 𝑦 } ) ≺ 𝐵 )
5 simp3 ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → 𝐵 ∈ Fin )
6 simp2 ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → 𝐴 ≈ 𝐵 )
7 enfii ⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵 ) → 𝐴 ∈ Fin )
8 5 6 7 syl2anc ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → 𝐴 ∈ Fin )
9 8 ad2antrr ⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝐴 ∈ Fin )
10 difssd ⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐴 ∖ { 𝑦 } ) ⊆ 𝐴 )
11 simplrr ⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑦 ∈ 𝐴 )
12 neldifsn ⊢ ¬ 𝑦 ∈ ( 𝐴 ∖ { 𝑦 } )
13 nelne1 ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ ( 𝐴 ∖ { 𝑦 } ) ) → 𝐴 ≠ ( 𝐴 ∖ { 𝑦 } ) )
14 11 12 13 sylancl ⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝐴 ≠ ( 𝐴 ∖ { 𝑦 } ) )
15 14 necomd ⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐴 ∖ { 𝑦 } ) ≠ 𝐴 )
16 df-pss ⊢ ( ( 𝐴 ∖ { 𝑦 } ) ⊊ 𝐴 ↔ ( ( 𝐴 ∖ { 𝑦 } ) ⊆ 𝐴 ∧ ( 𝐴 ∖ { 𝑦 } ) ≠ 𝐴 ) )
17 10 15 16 sylanbrc ⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐴 ∖ { 𝑦 } ) ⊊ 𝐴 )
18 php3 ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝐴 ∖ { 𝑦 } ) ⊊ 𝐴 ) → ( 𝐴 ∖ { 𝑦 } ) ≺ 𝐴 )
19 9 17 18 syl2anc ⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐴 ∖ { 𝑦 } ) ≺ 𝐴 )
20 6 ad2antrr ⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝐴 ≈ 𝐵 )
21 sdomentr ⊢ ( ( ( 𝐴 ∖ { 𝑦 } ) ≺ 𝐴 ∧ 𝐴 ≈ 𝐵 ) → ( 𝐴 ∖ { 𝑦 } ) ≺ 𝐵 )
22 19 20 21 syl2anc ⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐴 ∖ { 𝑦 } ) ≺ 𝐵 )
23 4 22 nsyl3 ⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ¬ 𝐵 ≼ ( 𝐴 ∖ { 𝑦 } ) )
24 8 adantr ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ) → 𝐴 ∈ Fin )
25 difss ⊢ ( 𝐴 ∖ { 𝑦 } ) ⊆ 𝐴
26 ssfi ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝐴 ∖ { 𝑦 } ) ⊆ 𝐴 ) → ( 𝐴 ∖ { 𝑦 } ) ∈ Fin )
27 24 25 26 sylancl ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ) → ( 𝐴 ∖ { 𝑦 } ) ∈ Fin )
28 3 adantr ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
29 fssres ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝐴 ∖ { 𝑦 } ) ⊆ 𝐴 ) → ( 𝐹 ↾ ( 𝐴 ∖ { 𝑦 } ) ) : ( 𝐴 ∖ { 𝑦 } ) ⟶ 𝐵 )
30 28 25 29 sylancl ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ) → ( 𝐹 ↾ ( 𝐴 ∖ { 𝑦 } ) ) : ( 𝐴 ∖ { 𝑦 } ) ⟶ 𝐵 )
31 1 adantr ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ) → 𝐹 : 𝐴 –onto→ 𝐵 )
32 foelrn ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ∃ 𝑢 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑢 ) )
33 31 32 sylan ⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ) ∧ 𝑧 ∈ 𝐵 ) → ∃ 𝑢 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑢 ) )
34 simprll ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ) → 𝑥 ∈ 𝐴 )
35 simprrr ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ) → 𝑥 ≠ 𝑦 )
36 eldifsn ⊢ ( 𝑥 ∈ ( 𝐴 ∖ { 𝑦 } ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦 ) )
37 34 35 36 sylanbrc ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ) → 𝑥 ∈ ( 𝐴 ∖ { 𝑦 } ) )
38 simprrl ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
39 38 eqcomd ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
40 fveq2 ⊢ ( 𝑤 = 𝑥 → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑥 ) )
41 40 rspceeqv ⊢ ( ( 𝑥 ∈ ( 𝐴 ∖ { 𝑦 } ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) → ∃ 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑤 ) )
42 37 39 41 syl2anc ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ) → ∃ 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑤 ) )
43 fveqeq2 ⊢ ( 𝑢 = 𝑦 → ( ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑤 ) ) )
44 43 rexbidv ⊢ ( 𝑢 = 𝑦 → ( ∃ 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑤 ) ↔ ∃ 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑤 ) ) )
45 42 44 syl5ibrcom ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ) → ( 𝑢 = 𝑦 → ∃ 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑤 ) ) )
46 45 adantr ⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ) ∧ 𝑢 ∈ 𝐴 ) → ( 𝑢 = 𝑦 → ∃ 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑤 ) ) )
47 46 imp ⊢ ( ( ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑢 = 𝑦 ) → ∃ 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑤 ) )
48 eldifsn ⊢ ( 𝑢 ∈ ( 𝐴 ∖ { 𝑦 } ) ↔ ( 𝑢 ∈ 𝐴 ∧ 𝑢 ≠ 𝑦 ) )
49 eqid ⊢ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑢 )
50 fveq2 ⊢ ( 𝑤 = 𝑢 → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑢 ) )
51 50 rspceeqv ⊢ ( ( 𝑢 ∈ ( 𝐴 ∖ { 𝑦 } ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑢 ) ) → ∃ 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑤 ) )
52 49 51 mpan2 ⊢ ( 𝑢 ∈ ( 𝐴 ∖ { 𝑦 } ) → ∃ 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑤 ) )
53 48 52 sylbir ⊢ ( ( 𝑢 ∈ 𝐴 ∧ 𝑢 ≠ 𝑦 ) → ∃ 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑤 ) )
54 53 adantll ⊢ ( ( ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑢 ≠ 𝑦 ) → ∃ 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑤 ) )
55 47 54 pm2.61dane ⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ) ∧ 𝑢 ∈ 𝐴 ) → ∃ 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑤 ) )
56 fvres ⊢ ( 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) → ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑦 } ) ) ‘ 𝑤 ) = ( 𝐹 ‘ 𝑤 ) )
57 56 eqeq2d ⊢ ( 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) → ( 𝑧 = ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑦 } ) ) ‘ 𝑤 ) ↔ 𝑧 = ( 𝐹 ‘ 𝑤 ) ) )
58 57 rexbiia ⊢ ( ∃ 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) 𝑧 = ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑦 } ) ) ‘ 𝑤 ) ↔ ∃ 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) 𝑧 = ( 𝐹 ‘ 𝑤 ) )
59 eqeq1 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑢 ) → ( 𝑧 = ( 𝐹 ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑤 ) ) )
60 59 rexbidv ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑢 ) → ( ∃ 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) 𝑧 = ( 𝐹 ‘ 𝑤 ) ↔ ∃ 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑤 ) ) )
61 58 60 bitrid ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑢 ) → ( ∃ 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) 𝑧 = ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑦 } ) ) ‘ 𝑤 ) ↔ ∃ 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑤 ) ) )
62 55 61 syl5ibrcom ⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ) ∧ 𝑢 ∈ 𝐴 ) → ( 𝑧 = ( 𝐹 ‘ 𝑢 ) → ∃ 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) 𝑧 = ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑦 } ) ) ‘ 𝑤 ) ) )
63 62 rexlimdva ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ) → ( ∃ 𝑢 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑢 ) → ∃ 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) 𝑧 = ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑦 } ) ) ‘ 𝑤 ) ) )
64 63 imp ⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ) ∧ ∃ 𝑢 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑢 ) ) → ∃ 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) 𝑧 = ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑦 } ) ) ‘ 𝑤 ) )
65 33 64 syldan ⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ) ∧ 𝑧 ∈ 𝐵 ) → ∃ 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) 𝑧 = ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑦 } ) ) ‘ 𝑤 ) )
66 65 ralrimiva ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ) → ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) 𝑧 = ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑦 } ) ) ‘ 𝑤 ) )
67 dffo3 ⊢ ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑦 } ) ) : ( 𝐴 ∖ { 𝑦 } ) –onto→ 𝐵 ↔ ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑦 } ) ) : ( 𝐴 ∖ { 𝑦 } ) ⟶ 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) 𝑧 = ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑦 } ) ) ‘ 𝑤 ) ) )
68 30 66 67 sylanbrc ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ) → ( 𝐹 ↾ ( 𝐴 ∖ { 𝑦 } ) ) : ( 𝐴 ∖ { 𝑦 } ) –onto→ 𝐵 )
69 fodomfi ⊢ ( ( ( 𝐴 ∖ { 𝑦 } ) ∈ Fin ∧ ( 𝐹 ↾ ( 𝐴 ∖ { 𝑦 } ) ) : ( 𝐴 ∖ { 𝑦 } ) –onto→ 𝐵 ) → 𝐵 ≼ ( 𝐴 ∖ { 𝑦 } ) )
70 27 68 69 syl2anc ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ) → 𝐵 ≼ ( 𝐴 ∖ { 𝑦 } ) )
71 70 anassrs ⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝐵 ≼ ( 𝐴 ∖ { 𝑦 } ) )
72 71 expr ⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝑥 ≠ 𝑦 → 𝐵 ≼ ( 𝐴 ∖ { 𝑦 } ) ) )
73 72 necon1bd ⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( ¬ 𝐵 ≼ ( 𝐴 ∖ { 𝑦 } ) → 𝑥 = 𝑦 ) )
74 23 73 mpd ⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑥 = 𝑦 )
75 74 ex ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
76 75 ralrimivva ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
77 dff13 ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
78 3 76 77 sylanbrc ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → 𝐹 : 𝐴 –1-1→ 𝐵 )
79 df-f1o ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) )
80 78 1 79 sylanbrc ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )