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.

Step	Hyp	Ref	Expression
1		simp1 958	. . . 4
2		fof 5700	. . . 4
3	1, 2	syl 16	. . 3
4		domnsym 7282	. . . . . . 7
5		simp3 960	. . . . . . . . . . 11
6		simp2 959	. . . . . . . . . . 11
7		enfii 7375	. . . . . . . . . . 11
8	5, 6, 7	syl2anc 644	. . . . . . . . . 10
9	8	ad2antrr 708	. . . . . . . . 9
10		difssd 3464	. . . . . . . . . 10
11		simplrr 739	. . . . . . . . . . . 12
12		neldifsn 3957	. . . . . . . . . . . 12
13		nelne1 2700	. . . . . . . . . . . 12
14	11, 12, 13	sylancl 645	. . . . . . . . . . 11
15	14	necomd 2694	. . . . . . . . . 10
16		df-pss 3325	. . . . . . . . . 10
17	10, 15, 16	sylanbrc 647	. . . . . . . . 9
18		php3 7342	. . . . . . . . 9
19	9, 17, 18	syl2anc 644	. . . . . . . 8
20	6	ad2antrr 708	. . . . . . . 8
21		sdomentr 7290	. . . . . . . 8
22	19, 20, 21	syl2anc 644	. . . . . . 7
23	4, 22	nsyl3 114	. . . . . 6
24	8	adantr 453	. . . . . . . . . . 11
25		difss 3463	. . . . . . . . . . 11
26		ssfi 7378	. . . . . . . . . . 11
27	24, 25, 26	sylancl 645	. . . . . . . . . 10
28	3	adantr 453	. . . . . . . . . . . 12
29		fssres 5657	. . . . . . . . . . . 12
30	28, 25, 29	sylancl 645	. . . . . . . . . . 11
31	1	adantr 453	. . . . . . . . . . . . . 14
32		foelrn 5936	. . . . . . . . . . . . . 14
33	31, 32	sylan 459	. . . . . . . . . . . . 13
34		simprll 740	. . . . . . . . . . . . . . . . . . . . . 22
35		simprrr 743	. . . . . . . . . . . . . . . . . . . . . 22
36		eldifsn 3955	. . . . . . . . . . . . . . . . . . . . . 22
37	34, 35, 36	sylanbrc 647	. . . . . . . . . . . . . . . . . . . . 21
38		simprrl 742	. . . . . . . . . . . . . . . . . . . . . 22
39	38	eqcomd 2448	. . . . . . . . . . . . . . . . . . . . 21
40		fveq2 5775	. . . . . . . . . . . . . . . . . . . . . . 23
41	40	eqeq2d 2454	. . . . . . . . . . . . . . . . . . . . . 22
42	41	rspcev 3061	. . . . . . . . . . . . . . . . . . . . 21
43	37, 39, 42	syl2anc 644	. . . . . . . . . . . . . . . . . . . 20
44		fveq2 5775	. . . . . . . . . . . . . . . . . . . . . 22
45	44	eqeq1d 2451	. . . . . . . . . . . . . . . . . . . . 21
46	45	rexbidv 2733	. . . . . . . . . . . . . . . . . . . 20
47	43, 46	syl5ibrcom 215	. . . . . . . . . . . . . . . . . . 19
48	47	adantr 453	. . . . . . . . . . . . . . . . . 18
49	48	imp 420	. . . . . . . . . . . . . . . . 17
50		eldifsn 3955	. . . . . . . . . . . . . . . . . . 19
51		eqid 2443	. . . . . . . . . . . . . . . . . . . 20
52		fveq2 5775	. . . . . . . . . . . . . . . . . . . . . 22
53	52	eqeq2d 2454	. . . . . . . . . . . . . . . . . . . . 21
54	53	rspcev 3061	. . . . . . . . . . . . . . . . . . . 20
55	51, 54	mpan2 654	. . . . . . . . . . . . . . . . . . 19
56	50, 55	sylbir 206	. . . . . . . . . . . . . . . . . 18
57	56	adantll 696	. . . . . . . . . . . . . . . . 17
58	49, 57	pm2.61dane 2689	. . . . . . . . . . . . . . . 16
59		fvres 5788	. . . . . . . . . . . . . . . . . . 19
60	59	eqeq2d 2454	. . . . . . . . . . . . . . . . . 18
61	60	rexbiia 2745	. . . . . . . . . . . . . . . . 17
62		eqeq1 2449	. . . . . . . . . . . . . . . . . 18
63	62	rexbidv 2733	. . . . . . . . . . . . . . . . 17
64	61, 63	syl5bb 250	. . . . . . . . . . . . . . . 16
65	58, 64	syl5ibrcom 215	. . . . . . . . . . . . . . 15
66	65	rexlimdva 2837	. . . . . . . . . . . . . 14
67	66	imp 420	. . . . . . . . . . . . 13
68	33, 67	syldan 458	. . . . . . . . . . . 12
69	68	ralrimiva 2796	. . . . . . . . . . 11
70		dffo3 5932	. . . . . . . . . . 11
71	30, 69, 70	sylanbrc 647	. . . . . . . . . 10
72		fodomfi 7434	. . . . . . . . . 10
73	27, 71, 72	syl2anc 644	. . . . . . . . 9
74	73	anassrs 631	. . . . . . . 8
75	74	expr 600	. . . . . . 7
76	75	necon1bd 2679	. . . . . 6
77	23, 76	mpd 15	. . . . 5
78	77	ex 425	. . . 4
79	78	ralrimivva 2805	. . 3
80		dff13 6052	. . 3
81	3, 79, 80	sylanbrc 647	. 2
82		df-f1o 5508	. 2
83	81, 1, 82	sylanbrc 647	1

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