MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fofinf1o Unicode version

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

Proof of Theorem fofinf1o
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp1 958 . . . 4
2 fof 5700 . . . 4
31, 2syl 16 . . 3
4 domnsym 7282 . . . . . . 7
5 simp3 960 . . . . . . . . . . 11
6 simp2 959 . . . . . . . . . . 11
7 enfii 7375 . . . . . . . . . . 11
85, 6, 7syl2anc 644 . . . . . . . . . 10
98ad2antrr 708 . . . . . . . . 9
10 difssd 3464 . . . . . . . . . 10
11 simplrr 739 . . . . . . . . . . . 12
12 neldifsn 3957 . . . . . . . . . . . 12
13 nelne1 2700 . . . . . . . . . . . 12
1411, 12, 13sylancl 645 . . . . . . . . . . 11
1514necomd 2694 . . . . . . . . . 10
16 df-pss 3325 . . . . . . . . . 10
1710, 15, 16sylanbrc 647 . . . . . . . . 9
18 php3 7342 . . . . . . . . 9
199, 17, 18syl2anc 644 . . . . . . . 8
206ad2antrr 708 . . . . . . . 8
21 sdomentr 7290 . . . . . . . 8
2219, 20, 21syl2anc 644 . . . . . . 7
234, 22nsyl3 114 . . . . . 6
248adantr 453 . . . . . . . . . . 11
25 difss 3463 . . . . . . . . . . 11
26 ssfi 7378 . . . . . . . . . . 11
2724, 25, 26sylancl 645 . . . . . . . . . 10
283adantr 453 . . . . . . . . . . . 12
29 fssres 5657 . . . . . . . . . . . 12
3028, 25, 29sylancl 645 . . . . . . . . . . 11
311adantr 453 . . . . . . . . . . . . . 14
32 foelrn 5936 . . . . . . . . . . . . . 14
3331, 32sylan 459 . . . . . . . . . . . . 13
34 simprll 740 . . . . . . . . . . . . . . . . . . . . . 22
35 simprrr 743 . . . . . . . . . . . . . . . . . . . . . 22
36 eldifsn 3955 . . . . . . . . . . . . . . . . . . . . . 22
3734, 35, 36sylanbrc 647 . . . . . . . . . . . . . . . . . . . . 21
38 simprrl 742 . . . . . . . . . . . . . . . . . . . . . 22
3938eqcomd 2448 . . . . . . . . . . . . . . . . . . . . 21
40 fveq2 5775 . . . . . . . . . . . . . . . . . . . . . . 23
4140eqeq2d 2454 . . . . . . . . . . . . . . . . . . . . . 22
4241rspcev 3061 . . . . . . . . . . . . . . . . . . . . 21
4337, 39, 42syl2anc 644 . . . . . . . . . . . . . . . . . . . 20
44 fveq2 5775 . . . . . . . . . . . . . . . . . . . . . 22
4544eqeq1d 2451 . . . . . . . . . . . . . . . . . . . . 21
4645rexbidv 2733 . . . . . . . . . . . . . . . . . . . 20
4743, 46syl5ibrcom 215 . . . . . . . . . . . . . . . . . . 19
4847adantr 453 . . . . . . . . . . . . . . . . . 18
4948imp 420 . . . . . . . . . . . . . . . . 17
50 eldifsn 3955 . . . . . . . . . . . . . . . . . . 19
51 eqid 2443 . . . . . . . . . . . . . . . . . . . 20
52 fveq2 5775 . . . . . . . . . . . . . . . . . . . . . 22
5352eqeq2d 2454 . . . . . . . . . . . . . . . . . . . . 21
5453rspcev 3061 . . . . . . . . . . . . . . . . . . . 20
5551, 54mpan2 654 . . . . . . . . . . . . . . . . . . 19
5650, 55sylbir 206 . . . . . . . . . . . . . . . . . 18
5756adantll 696 . . . . . . . . . . . . . . . . 17
5849, 57pm2.61dane 2689 . . . . . . . . . . . . . . . 16
59 fvres 5788 . . . . . . . . . . . . . . . . . . 19
6059eqeq2d 2454 . . . . . . . . . . . . . . . . . 18
6160rexbiia 2745 . . . . . . . . . . . . . . . . 17
62 eqeq1 2449 . . . . . . . . . . . . . . . . . 18
6362rexbidv 2733 . . . . . . . . . . . . . . . . 17
6461, 63syl5bb 250 . . . . . . . . . . . . . . . 16
6558, 64syl5ibrcom 215 . . . . . . . . . . . . . . 15
6665rexlimdva 2837 . . . . . . . . . . . . . 14
6766imp 420 . . . . . . . . . . . . 13
6833, 67syldan 458 . . . . . . . . . . . 12
6968ralrimiva 2796 . . . . . . . . . . 11
70 dffo3 5932 . . . . . . . . . . 11
7130, 69, 70sylanbrc 647 . . . . . . . . . 10
72 fodomfi 7434 . . . . . . . . . 10
7327, 71, 72syl2anc 644 . . . . . . . . 9
7473anassrs 631 . . . . . . . 8
7574expr 600 . . . . . . 7
7675necon1bd 2679 . . . . . 6
7723, 76mpd 15 . . . . 5
7877ex 425 . . . 4
7978ralrimivva 2805 . . 3
80 dff13 6052 . . 3
813, 79, 80sylanbrc 647 . 2
82 df-f1o 5508 . 2
8381, 1, 82sylanbrc 647 1
Colors of variables: wff set class
Syntax hints:  -.wn 3  ->wi 4  /\wa 360  /\w3a 937  =wceq 1654  e.wcel 1728  =/=wne 2606  A.wral 2712  E.wrex 2713  \cdif 3306  C_wss 3309  C.wpss 3310  {csn 3841   class class class wbr 4243  |`cres 4921  -->wf 5497  -1-1->wf1 5498  -onto->wfo 5499  -1-1-onto->wf1o 5500  `cfv 5501   cen 7155   cdom 7156   csdm 7157   cfn 7158
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-13 1730  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424  ax-sep 4364  ax-nul 4372  ax-pow 4416  ax-pr 4442  ax-un 4742
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-eu 2292  df-mo 2293  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2717  df-rex 2718  df-reu 2719  df-rab 2721  df-v 2967  df-sbc 3171  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-pss 3325  df-nul 3617  df-if 3766  df-pw 3828  df-sn 3847  df-pr 3848  df-tp 3849  df-op 3850  df-uni 4044  df-br 4244  df-opab 4302  df-mpt 4303  df-tr 4337  df-eprel 4535  df-id 4539  df-po 4544  df-so 4545  df-fr 4582  df-we 4584  df-ord 4625  df-on 4626  df-lim 4627  df-suc 4628  df-om 4887  df-xp 4925  df-rel 4926  df-cnv 4927  df-co 4928  df-dm 4929  df-rn 4930  df-res 4931  df-ima 4932  df-iota 5464  df-fun 5503  df-fn 5504  df-f 5505  df-f1 5506  df-fo 5507  df-f1o 5508  df-fv 5509  df-1o 6773  df-er 6954  df-en 7159  df-dom 7160  df-sdom 7161  df-fin 7162
  Copyright terms: Public domain W3C validator