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 syl5bb ( 𝑧 = ( 𝐹𝑢 ) → ( ∃ 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) 𝑧 = ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑦 } ) ) ‘ 𝑤 ) ↔ ∃ 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) ( 𝐹𝑢 ) = ( 𝐹𝑤 ) ) )
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𝐵 )