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

Theorem dfac5 8002
 Description: Equivalence of two versions of the Axiom of Choice. The right-hand side is Theorem 6M(4) of [Enderton] p. 151 and asserts that given a family of mutually disjoint nonempty sets, a set exists containing exactly one member from each set in the family. The proof does not depend on AC. (Contributed by NM, 11-Apr-2004.) (Revised by Mario Carneiro, 17-May-2015.)
Assertion
Ref Expression
dfac5 CHOICE
Distinct variable group:   ,,,,

Proof of Theorem dfac5
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfac4 7996 . . 3 CHOICE
2 neeq1 2607 . . . . . . . . . . . . 13
32cbvralv 2925 . . . . . . . . . . . 12
43anbi2i 676 . . . . . . . . . . 11
5 r19.26 2831 . . . . . . . . . . 11
64, 5bitr4i 244 . . . . . . . . . 10
7 pm3.35 571 . . . . . . . . . . . 12
87ancoms 440 . . . . . . . . . . 11
98ralimi 2774 . . . . . . . . . 10
106, 9sylbi 188 . . . . . . . . 9
11 r19.26 2831 . . . . . . . . . . . . . . . . . 18
12 elin 3523 . . . . . . . . . . . . . . . . . . 19
13 fvelrnb 5767 . . . . . . . . . . . . . . . . . . . . . . . 24
1413biimpac 473 . . . . . . . . . . . . . . . . . . . . . . 23
15 fveq2 5721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
16 id 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
1715, 16eleq12d 2504 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
18 neeq2 2608 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
19 ineq2 3529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
2019eqeq1d 2444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2118, 20imbi12d 312 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2217, 21anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2322rspcv 3041 . . . . . . . . . . . . . . . . . . . . . . . . . 26
24 eleq1 2496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
2524biimpar 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
26 minel 3676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
2726ex 424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
2827imim2d 50 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
2928imp 419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
3029necon4ad 2660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
3130imp 419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
3225, 31sylan2 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
33 fveq2 5721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
34 eqeq2 2445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
35 eqcom 2438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
3634, 35syl6bb 253 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
3733, 36syl5ib 211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
3837ad2antrl 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3932, 38mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
4039exp32 589 . . . . . . . . . . . . . . . . . . . . . . . . . 26
4123, 40syl6com 33 . . . . . . . . . . . . . . . . . . . . . . . . 25
4241com14 84 . . . . . . . . . . . . . . . . . . . . . . . 24
4342rexlimdv 2822 . . . . . . . . . . . . . . . . . . . . . . 23
4414, 43syl5 30 . . . . . . . . . . . . . . . . . . . . . 22
4544exp3a 426 . . . . . . . . . . . . . . . . . . . . 21
4645com4t 81 . . . . . . . . . . . . . . . . . . . 20
4746imp4b 574 . . . . . . . . . . . . . . . . . . 19
4812, 47syl5bi 209 . . . . . . . . . . . . . . . . . 18
4911, 48sylan2br 463 . . . . . . . . . . . . . . . . 17
5049anassrs 630 . . . . . . . . . . . . . . . 16
5150adantlr 696 . . . . . . . . . . . . . . 15
52 fveq2 5721 . . . . . . . . . . . . . . . . . . . . . . . 24
53 id 20 . . . . . . . . . . . . . . . . . . . . . . . 24
5452, 53eleq12d 2504 . . . . . . . . . . . . . . . . . . . . . . 23
5554rspcv 3041 . . . . . . . . . . . . . . . . . . . . . 22
56 fnfvelrn 5860 . . . . . . . . . . . . . . . . . . . . . . 23
5756expcom 425 . . . . . . . . . . . . . . . . . . . . . 22
5855, 57anim12d 547 . . . . . . . . . . . . . . . . . . . . 21
59 elin 3523 . . . . . . . . . . . . . . . . . . . . 21
6058, 59syl6ibr 219 . . . . . . . . . . . . . . . . . . . 20
6160exp3a 426 . . . . . . . . . . . . . . . . . . 19
6261com13 76 . . . . . . . . . . . . . . . . . 18
6362imp31 422 . . . . . . . . . . . . . . . . 17
64 eleq1 2496 . . . . . . . . . . . . . . . . 17
6563, 64syl5ibrcom 214 . . . . . . . . . . . . . . . 16
6665adantr 452 . . . . . . . . . . . . . . 15
6751, 66impbid 184 . . . . . . . . . . . . . 14
6867ex 424 . . . . . . . . . . . . 13
6968alrimdv 1643 . . . . . . . . . . . 12
70 fvex 5735 . . . . . . . . . . . . . 14
71 eqeq2 2445 . . . . . . . . . . . . . . . 16
7271bibi2d 310 . . . . . . . . . . . . . . 15
7372albidv 1635 . . . . . . . . . . . . . 14
7470, 73spcev 3036 . . . . . . . . . . . . 13
75 df-eu 2285 . . . . . . . . . . . . 13
7674, 75sylibr 204 . . . . . . . . . . . 12
7769, 76syl6 31 . . . . . . . . . . 11
7877ralimdva 2777 . . . . . . . . . 10
7978ex 424 . . . . . . . . 9
8010, 79syl5 30 . . . . . . . 8
8180exp3a 426 . . . . . . 7
8281imp4b 574 . . . . . 6
83 vex 2952 . . . . . . . 8
8483rnex 5126 . . . . . . 7
85 ineq2 3529 . . . . . . . . . 10
8685eleq2d 2503 . . . . . . . . 9
8786eubidv 2289 . . . . . . . 8
8887ralbidv 2718 . . . . . . 7
8984, 88spcev 3036 . . . . . 6
9082, 89syl6 31 . . . . 5
9190exlimiv 1644 . . . 4
9291alimi 1568 . . 3
931, 92sylbi 188 . 2 CHOICE
94 eqid 2436 . . . . 5
95 eqid 2436 . . . . 5
96 biid 228 . . . . 5
9794, 95, 96dfac5lem5 8001 . . . 4
9897alrimiv 1641 . . 3
99 dfac3 7995 . . 3 CHOICE
10098, 99sylibr 204 . 2 CHOICE
10193, 100impbii 181 1 CHOICE
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wa 359  wal 1549  wex 1550   wceq 1652   wcel 1725  weu 2281  cab 2422   wne 2599  wral 2698  wrex 2699   cin 3312  c0 3621  csn 3807  cuni 4008   cxp 4869   crn 4872   wfn 5442  cfv 5447  CHOICEwac 7989 This theorem is referenced by:  dfackm  8039  ac8  8365 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-sep 4323  ax-nul 4331  ax-pow 4370  ax-pr 4396  ax-un 4694 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2703  df-rex 2704  df-rab 2707  df-v 2951  df-sbc 3155  df-csb 3245  df-dif 3316  df-un 3318  df-in 3320  df-ss 3327  df-nul 3622  df-if 3733  df-pw 3794  df-sn 3813  df-pr 3814  df-op 3816  df-uni 4009  df-br 4206  df-opab 4260  df-mpt 4261  df-id 4491  df-xp 4877  df-rel 4878  df-cnv 4879  df-co 4880  df-dm 4881  df-rn 4882  df-res 4883  df-ima 4884  df-iota 5411  df-fun 5449  df-fn 5450  df-f 5451  df-fv 5455  df-ac 7990
 Copyright terms: Public domain W3C validator