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

Theorem ac6num 8364
 Description: A version of ac6 8365 which takes the choice as a hypothesis. (Contributed by Mario Carneiro, 27-Aug-2015.)
Hypothesis
Ref Expression
ac6num.1
Assertion
Ref Expression
ac6num
Distinct variable groups:   ,,   ,,,   ,   ,
Allowed substitution hints:   (,)   (,)   ()   (,,)

Proof of Theorem ac6num
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfiu1 4123 . . . . . . . . 9
21nfel1 2584 . . . . . . . 8
3 ssiun2 4136 . . . . . . . . 9
4 ssexg 4352 . . . . . . . . . 10
54expcom 426 . . . . . . . . 9
63, 5syl5 31 . . . . . . . 8
72, 6ralrimi 2789 . . . . . . 7
8 dfiun2g 4125 . . . . . . 7
97, 8syl 16 . . . . . 6
10 eqid 2438 . . . . . . . 8
1110rnmpt 5119 . . . . . . 7
1211unieqi 4027 . . . . . 6
139, 12syl6eqr 2488 . . . . 5
14 id 21 . . . . 5
1513, 14eqeltrrd 2513 . . . 4
17 simp3 960 . . . . 5
18 necom 2687 . . . . . . . 8
19 rabn0 3649 . . . . . . . 8
20 df-ne 2603 . . . . . . . 8
2118, 19, 203bitr3i 268 . . . . . . 7
2221ralbii 2731 . . . . . 6
23 ralnex 2717 . . . . . 6
2422, 23bitri 242 . . . . 5
2517, 24sylib 190 . . . 4
26 0ex 4342 . . . . 5
2710elrnmpt 5120 . . . . 5
2826, 27ax-mp 5 . . . 4
2925, 28sylnibr 298 . . 3
30 ac5num 7922 . . 3
3116, 29, 30syl2anc 644 . 2
32 ffn 5594 . . . . . 6
3332anim1i 553 . . . . 5
3473ad2ant2 980 . . . . . . 7
35 fveq2 5731 . . . . . . . . 9
36 id 21 . . . . . . . . 9
3735, 36eleq12d 2506 . . . . . . . 8
3810, 37ralrnmpt 5881 . . . . . . 7
3934, 38syl 16 . . . . . 6
4039anbi2d 686 . . . . 5
4133, 40syl5ib 212 . . . 4
423sseld 3349 . . . . . . . . . . 11
4342ralimia 2781 . . . . . . . . . 10
4443ad2antll 711 . . . . . . . . 9
45 nfv 1630 . . . . . . . . . 10
46 nfcsb1v 3285 . . . . . . . . . . 11
4746, 1nfel 2582 . . . . . . . . . 10
48 csbeq1a 3261 . . . . . . . . . . 11
4948eleq1d 2504 . . . . . . . . . 10
5045, 47, 49cbvral 2930 . . . . . . . . 9
5144, 50sylib 190 . . . . . . . 8
52 nfcv 2574 . . . . . . . . . 10
5352, 46, 48cbvmpt 4302 . . . . . . . . 9
5453fmpt 5893 . . . . . . . 8
5551, 54sylib 190 . . . . . . 7
56 simpl1 961 . . . . . . 7
57 simpl2 962 . . . . . . 7
58 fex2 5606 . . . . . . 7
5955, 56, 57, 58syl3anc 1185 . . . . . 6
60 ssrab2 3430 . . . . . . . . . . 11
6160sseli 3346 . . . . . . . . . 10
6261ralimi 2783 . . . . . . . . 9
6362ad2antll 711 . . . . . . . 8
64 eqid 2438 . . . . . . . . 9
6564fmpt 5893 . . . . . . . 8
6663, 65sylib 190 . . . . . . 7
67 nfcv 2574 . . . . . . . . . . 11
6867elrabsf 3201 . . . . . . . . . 10
6968simprbi 452 . . . . . . . . 9
7069ralimi 2783 . . . . . . . 8
7170ad2antll 711 . . . . . . 7
7266, 71jca 520 . . . . . 6
73 feq1 5579 . . . . . . . 8
74 nfmpt1 4301 . . . . . . . . . 10
7574nfeq2 2585 . . . . . . . . 9
76 fvex 5745 . . . . . . . . . . 11
77 ac6num.1 . . . . . . . . . . 11
7876, 77sbcie 3197 . . . . . . . . . 10
79 fveq1 5730 . . . . . . . . . . . 12
80 fvex 5745 . . . . . . . . . . . . 13
8164fvmpt2 5815 . . . . . . . . . . . . 13
8280, 81mpan2 654 . . . . . . . . . . . 12
8379, 82sylan9eq 2490 . . . . . . . . . . 11
84 dfsbcq 3165 . . . . . . . . . . 11
8583, 84syl 16 . . . . . . . . . 10
8678, 85syl5bbr 252 . . . . . . . . 9
8775, 86ralbida 2721 . . . . . . . 8
8873, 87anbi12d 693 . . . . . . 7
8988spcegv 3039 . . . . . 6
9059, 72, 89sylc 59 . . . . 5
9190ex 425 . . . 4
9241, 91syld 43 . . 3
9392exlimdv 1647 . 2
9431, 93mpd 15 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 178   wa 360   w3a 937  wex 1551   wceq 1653   wcel 1726  cab 2424   wne 2601  wral 2707  wrex 2708  crab 2711  cvv 2958  wsbc 3163  csb 3253   wss 3322  c0 3630  cuni 4017  ciun 4095   cmpt 4269   cdm 4881   crn 4882   wfn 5452  wf 5453  cfv 5457  ccrd 7827 This theorem is referenced by:  ac6  8365  ptcmplem3  18090 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 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4323  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704 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 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-int 4053  df-iun 4097  df-br 4216  df-opab 4270  df-mpt 4271  df-tr 4306  df-eprel 4497  df-id 4501  df-po 4506  df-so 4507  df-fr 4544  df-se 4545  df-we 4546  df-ord 4587  df-on 4588  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-isom 5466  df-riota 6552  df-en 7113  df-card 7831
 Copyright terms: Public domain W3C validator