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

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.
StepHypRef Expression
1 raleq 3054 . . . 4
2 feq2 5719 . . . . . 6
3 raleq 3054 . . . . . 6
42, 3anbi12d 710 . . . . 5
54exbidv 1714 . . . 4
61, 5imbi12d 320 . . 3
7 raleq 3054 . . . 4
8 feq2 5719 . . . . . 6
9 raleq 3054 . . . . . 6
108, 9anbi12d 710 . . . . 5
1110exbidv 1714 . . . 4
127, 11imbi12d 320 . . 3
13 raleq 3054 . . . 4
14 feq2 5719 . . . . . . 7
15 raleq 3054 . . . . . . 7
1614, 15anbi12d 710 . . . . . 6
1716exbidv 1714 . . . . 5
18 feq1 5718 . . . . . . 7
19 fvex 5881 . . . . . . . . . 10
20 ac6sfi.1 . . . . . . . . . 10
2119, 20sbcie 3362 . . . . . . . . 9
22 fveq1 5870 . . . . . . . . . 10
2322sbceq1d 3332 . . . . . . . . 9
2421, 23syl5bbr 259 . . . . . . . 8
2524ralbidv 2896 . . . . . . 7
2618, 25anbi12d 710 . . . . . 6
2726cbvexv 2024 . . . . 5
2817, 27syl6bb 261 . . . 4
2913, 28imbi12d 320 . . 3
30 raleq 3054 . . . 4
31 feq2 5719 . . . . . 6
32 raleq 3054 . . . . . 6
3331, 32anbi12d 710 . . . . 5
3433exbidv 1714 . . . 4
3530, 34imbi12d 320 . . 3
36 f0 5771 . . . 4
37 0ex 4582 . . . . 5
38 ral0 3934 . . . . . . 7
3938biantru 505 . . . . . 6
40 feq1 5718 . . . . . 6
4139, 40syl5bbr 259 . . . . 5
4237, 41spcev 3201 . . . 4
4336, 42mp1i 12 . . 3
44 ssun1 3666 . . . . . . 7
45 ssralv 3563 . . . . . . 7
4644, 45ax-mp 5 . . . . . 6
4746imim1i 58 . . . . 5
48 ssun2 3667 . . . . . . . . 9
49 ssralv 3563 . . . . . . . . 9
5048, 49ax-mp 5 . . . . . . . 8
51 vex 3112 . . . . . . . . . 10
52 ralsnsg 4061 . . . . . . . . . 10
5351, 52ax-mp 5 . . . . . . . . 9
54 sbcrex 3412 . . . . . . . . 9
5553, 54bitri 249 . . . . . . . 8
5650, 55sylib 196 . . . . . . 7
57 nfv 1707 . . . . . . . 8
58 nfv 1707 . . . . . . . . 9
59 nfv 1707 . . . . . . . . . . 11
60 nfcv 2619 . . . . . . . . . . . 12
61 nfsbc1v 3347 . . . . . . . . . . . 12
6260, 61nfral 2843 . . . . . . . . . . 11
6359, 62nfan 1928 . . . . . . . . . 10
6463nfex 1948 . . . . . . . . 9
6558, 64nfim 1920 . . . . . . . 8
66 simprl 756 . . . . . . . . . . . . 13
67 vex 3112 . . . . . . . . . . . . . . . 16
6851, 67f1osn 5858 . . . . . . . . . . . . . . 15
69 f1of 5821 . . . . . . . . . . . . . . 15
7068, 69mp1i 12 . . . . . . . . . . . . . 14
71 simpl2 1000 . . . . . . . . . . . . . . 15
7271snssd 4175 . . . . . . . . . . . . . 14
7370, 72fssd 5745 . . . . . . . . . . . . 13
74 simpl1 999 . . . . . . . . . . . . . 14
75 disjsn 4090 . . . . . . . . . . . . . 14
7674, 75sylibr 212 . . . . . . . . . . . . 13
77 fun2 5754 . . . . . . . . . . . . 13
7866, 73, 76, 77syl21anc 1227 . . . . . . . . . . . 12
79 simprr 757 . . . . . . . . . . . . . 14
80 eleq1a 2540 . . . . . . . . . . . . . . . . . . 19
8180necon3bd 2669 . . . . . . . . . . . . . . . . . 18
8281impcom 430 . . . . . . . . . . . . . . . . 17
83 fvunsn 6103 . . . . . . . . . . . . . . . . 17
84 dfsbcq 3329 . . . . . . . . . . . . . . . . . 18
8584, 21syl6rbb 262 . . . . . . . . . . . . . . . . 17
8682, 83, 853syl 20 . . . . . . . . . . . . . . . 16
8786ralbidva 2893 . . . . . . . . . . . . . . 15
8874, 87syl 16 . . . . . . . . . . . . . 14
8979, 88mpbid 210 . . . . . . . . . . . . 13
90 simpl3 1001 . . . . . . . . . . . . . 14
91 ffun 5738 . . . . . . . . . . . . . . . . 17
92 ssun2 3667 . . . . . . . . . . . . . . . . . 18
93 ssnid 4058 . . . . . . . . . . . . . . . . . . 19
9467dmsnop 5487 . . . . . . . . . . . . . . . . . . 19
9593, 94eleqtrri 2544 . . . . . . . . . . . . . . . . . 18
96 funssfv 5886 . . . . . . . . . . . . . . . . . 18
9792, 95, 96mp3an23 1316 . . . . . . . . . . . . . . . . 17
9878, 91, 973syl 20 . . . . . . . . . . . . . . . 16
9951, 67fvsn 6104 . . . . . . . . . . . . . . . 16
10098, 99syl6req 2515 . . . . . . . . . . . . . . 15
101 ralsnsg 4061 . . . . . . . . . . . . . . . . 17
10251, 101ax-mp 5 . . . . . . . . . . . . . . . 16
103 elsni 4054 . . . . . . . . . . . . . . . . . . . . 21
104103fveq2d 5875 . . . . . . . . . . . . . . . . . . . 20
105104eqeq2d 2471 . . . . . . . . . . . . . . . . . . 19
106105biimparc 487 . . . . . . . . . . . . . . . . . 18
107 sbceq1a 3338 . . . . . . . . . . . . . . . . . 18
108106, 107syl 16 . . . . . . . . . . . . . . . . 17
109108ralbidva 2893 . . . . . . . . . . . . . . . 16
110102, 109syl5bbr 259 . . . . . . . . . . . . . . 15
111100, 110syl 16 . . . . . . . . . . . . . 14
11290, 111mpbid 210 . . . . . . . . . . . . 13
113 ralun 3685 . . . . . . . . . . . . 13
11489, 112, 113syl2anc 661 . . . . . . . . . . . 12
115 vex 3112 . . . . . . . . . . . . . 14
116 snex 4693 . . . . . . . . . . . . . 14
117115, 116unex 6598 . . . . . . . . . . . . 13
118 feq1 5718 . . . . . . . . . . . . . 14
119 fveq1 5870 . . . . . . . . . . . . . . . 16
120119sbceq1d 3332 . . . . . . . . . . . . . . 15
121120ralbidv 2896 . . . . . . . . . . . . . 14
122118, 121anbi12d 710 . . . . . . . . . . . . 13
123117, 122spcev 3201 . . . . . . . . . . . 12
12478, 114, 123syl2anc 661 . . . . . . . . . . 11
125124ex 434 . . . . . . . . . 10
126125exlimdv 1724 . . . . . . . . 9
1271263exp 1195 . . . . . . . 8
12857, 65, 127rexlimd 2941 . . . . . . 7
12956, 128syl5 32 . . . . . 6
130129a2d 26 . . . . 5
13147, 130syl5 32 . . . 4
132131adantl 466 . . 3
1336, 12, 29, 35, 43, 132findcard2s 7781 . 2
134133imp 429 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator