Theorem ac6sfi 7784

Description: A version of ac6s 8885 for finite sets. (Contributed by Jeff Hankins, 26-Jun-2009.) (Proof shortened by Mario Carneiro, 29-Jan-2014.)

Hypothesis

Ref	Expression
ac6sfi.1

Assertion

Ref	Expression
ac6sfi

Distinct variable groups:   ,,   ,,,   ,   ,

Proof of Theorem ac6sfi

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		raleq 3054	. . . 4
2		feq2 5719	. . . . . 6
3		raleq 3054	. . . . . 6
4	2, 3	anbi12d 710	. . . . 5
5	4	exbidv 1714	. . . 4
6	1, 5	imbi12d 320	. . 3
7		raleq 3054	. . . 4
8		feq2 5719	. . . . . 6
9		raleq 3054	. . . . . 6
10	8, 9	anbi12d 710	. . . . 5
11	10	exbidv 1714	. . . 4
12	7, 11	imbi12d 320	. . 3
13		raleq 3054	. . . 4
14		feq2 5719	. . . . . . 7
15		raleq 3054	. . . . . . 7
16	14, 15	anbi12d 710	. . . . . 6
17	16	exbidv 1714	. . . . 5
18		feq1 5718	. . . . . . 7
19		fvex 5881	. . . . . . . . . 10
20		ac6sfi.1	. . . . . . . . . 10
21	19, 20	sbcie 3362	. . . . . . . . 9
22		fveq1 5870	. . . . . . . . . 10
23	22	sbceq1d 3332	. . . . . . . . 9
24	21, 23	syl5bbr 259	. . . . . . . 8
25	24	ralbidv 2896	. . . . . . 7
26	18, 25	anbi12d 710	. . . . . 6
27	26	cbvexv 2024	. . . . 5
28	17, 27	syl6bb 261	. . . 4
29	13, 28	imbi12d 320	. . 3
30		raleq 3054	. . . 4
31		feq2 5719	. . . . . 6
32		raleq 3054	. . . . . 6
33	31, 32	anbi12d 710	. . . . 5
34	33	exbidv 1714	. . . 4
35	30, 34	imbi12d 320	. . 3
36		f0 5771	. . . 4
37		0ex 4582	. . . . 5
38		ral0 3934	. . . . . . 7
39	38	biantru 505	. . . . . 6
40		feq1 5718	. . . . . 6
41	39, 40	syl5bbr 259	. . . . 5
42	37, 41	spcev 3201	. . . 4
43	36, 42	mp1i 12	. . 3
44		ssun1 3666	. . . . . . 7
45		ssralv 3563	. . . . . . 7
46	44, 45	ax-mp 5	. . . . . 6
47	46	imim1i 58	. . . . 5
48		ssun2 3667	. . . . . . . . 9
49		ssralv 3563	. . . . . . . . 9
50	48, 49	ax-mp 5	. . . . . . . 8
51		vex 3112	. . . . . . . . . 10
52		ralsnsg 4061	. . . . . . . . . 10
53	51, 52	ax-mp 5	. . . . . . . . 9
54		sbcrex 3412	. . . . . . . . 9
55	53, 54	bitri 249	. . . . . . . 8
56	50, 55	sylib 196	. . . . . . 7
57		nfv 1707	. . . . . . . 8
58		nfv 1707	. . . . . . . . 9
59		nfv 1707	. . . . . . . . . . 11
60		nfcv 2619	. . . . . . . . . . . 12
61		nfsbc1v 3347	. . . . . . . . . . . 12
62	60, 61	nfral 2843	. . . . . . . . . . 11
63	59, 62	nfan 1928	. . . . . . . . . 10
64	63	nfex 1948	. . . . . . . . 9
65	58, 64	nfim 1920	. . . . . . . 8
66		simprl 756	. . . . . . . . . . . . 13
67		vex 3112	. . . . . . . . . . . . . . . 16
68	51, 67	f1osn 5858	. . . . . . . . . . . . . . 15
69		f1of 5821	. . . . . . . . . . . . . . 15
70	68, 69	mp1i 12	. . . . . . . . . . . . . 14
71		simpl2 1000	. . . . . . . . . . . . . . 15
72	71	snssd 4175	. . . . . . . . . . . . . 14
73	70, 72	fssd 5745	. . . . . . . . . . . . 13
74		simpl1 999	. . . . . . . . . . . . . 14
75		disjsn 4090	. . . . . . . . . . . . . 14
76	74, 75	sylibr 212	. . . . . . . . . . . . 13
77		fun2 5754	. . . . . . . . . . . . 13
78	66, 73, 76, 77	syl21anc 1227	. . . . . . . . . . . 12
79		simprr 757	. . . . . . . . . . . . . 14
80		eleq1a 2540	. . . . . . . . . . . . . . . . . . 19
81	80	necon3bd 2669	. . . . . . . . . . . . . . . . . 18
82	81	impcom 430	. . . . . . . . . . . . . . . . 17
83		fvunsn 6103	. . . . . . . . . . . . . . . . 17
84		dfsbcq 3329	. . . . . . . . . . . . . . . . . 18
85	84, 21	syl6rbb 262	. . . . . . . . . . . . . . . . 17
86	82, 83, 85	3syl 20	. . . . . . . . . . . . . . . 16
87	86	ralbidva 2893	. . . . . . . . . . . . . . 15
88	74, 87	syl 16	. . . . . . . . . . . . . 14
89	79, 88	mpbid 210	. . . . . . . . . . . . 13
90		simpl3 1001	. . . . . . . . . . . . . 14
91		ffun 5738	. . . . . . . . . . . . . . . . 17
92		ssun2 3667	. . . . . . . . . . . . . . . . . 18
93		ssnid 4058	. . . . . . . . . . . . . . . . . . 19
94	67	dmsnop 5487	. . . . . . . . . . . . . . . . . . 19
95	93, 94	eleqtrri 2544	. . . . . . . . . . . . . . . . . 18
96		funssfv 5886	. . . . . . . . . . . . . . . . . 18
97	92, 95, 96	mp3an23 1316	. . . . . . . . . . . . . . . . 17
98	78, 91, 97	3syl 20	. . . . . . . . . . . . . . . 16
99	51, 67	fvsn 6104	. . . . . . . . . . . . . . . 16
100	98, 99	syl6req 2515	. . . . . . . . . . . . . . 15
101		ralsnsg 4061	. . . . . . . . . . . . . . . . 17
102	51, 101	ax-mp 5	. . . . . . . . . . . . . . . 16
103		elsni 4054	. . . . . . . . . . . . . . . . . . . . 21
104	103	fveq2d 5875	. . . . . . . . . . . . . . . . . . . 20
105	104	eqeq2d 2471	. . . . . . . . . . . . . . . . . . 19
106	105	biimparc 487	. . . . . . . . . . . . . . . . . 18
107		sbceq1a 3338	. . . . . . . . . . . . . . . . . 18
108	106, 107	syl 16	. . . . . . . . . . . . . . . . 17
109	108	ralbidva 2893	. . . . . . . . . . . . . . . 16
110	102, 109	syl5bbr 259	. . . . . . . . . . . . . . 15
111	100, 110	syl 16	. . . . . . . . . . . . . 14
112	90, 111	mpbid 210	. . . . . . . . . . . . 13
113		ralun 3685	. . . . . . . . . . . . 13
114	89, 112, 113	syl2anc 661	. . . . . . . . . . . 12
115		vex 3112	. . . . . . . . . . . . . 14
116		snex 4693	. . . . . . . . . . . . . 14
117	115, 116	unex 6598	. . . . . . . . . . . . 13
118		feq1 5718	. . . . . . . . . . . . . 14
119		fveq1 5870	. . . . . . . . . . . . . . . 16
120	119	sbceq1d 3332	. . . . . . . . . . . . . . 15
121	120	ralbidv 2896	. . . . . . . . . . . . . 14
122	118, 121	anbi12d 710	. . . . . . . . . . . . 13
123	117, 122	spcev 3201	. . . . . . . . . . . 12
124	78, 114, 123	syl2anc 661	. . . . . . . . . . 11
125	124	ex 434	. . . . . . . . . 10
126	125	exlimdv 1724	. . . . . . . . 9
127	126	3exp 1195	. . . . . . . 8
128	57, 65, 127	rexlimd 2941	. . . . . . 7
129	56, 128	syl5 32	. . . . . 6
130	129	a2d 26	. . . . 5
131	47, 130	syl5 32	. . . 4
132	131	adantl 466	. . 3
133	6, 12, 29, 35, 43, 132	findcard2s 7781	. 2
134	133	imp 429	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  /\w3a 973  =wceq 1395  E.wex 1612  e.wcel 1818  =/=wne 2652  A.wral 2807  E.wrex 2808  cvv 3109  [.wsbc 3327  u.cun 3473  i^icin 3474  C_wss 3475  c0 3784  {csn 4029  <.cop 4035  domcdm 5004  Funwfun 5587  -->wf 5589  -1-1-onto->wf1o 5592  `cfv 5593  cfn 7536

This theorem is referenced by:  fissuni  7845  fipreima  7846  indexfi  7848  finacn  8452  axcc4dom  8842  ttukeylem6  8915  firest  14830  ablfaclem3  17138  ablfac2  17140  cmpcovf  19891  cmpsub  19900  tgcmp  19901  hauscmplem  19906  comppfsc  20033  ptcnplem  20122  alexsubALTlem3  20549  alexsubALT  20551  tsmsxplem1  20655  ovolicc2lem5  21932  ovolicc2  21933  limciun  22298  cvmliftlem15  28743  istotbnd3  30267  sstotbnd2  30270  sstotbnd  30271  prdsbnd  30289  prdstotbnd  30290  heiborlem1  30307  heibor  30317  kelac1  31009  hbt  31079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-om 6701  df-1o 7149  df-er 7330  df-en 7537  df-fin 7540