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

Theorem dfac2 8532
Description: Axiom of Choice (first form) of [Enderton] p. 49 implies of our Axiom of Choice (in the form of ac3 8863). The proof does not make use of AC. Note that the Axiom of Regularity is used by the proof. Specifically, elirrv 8044 and preleq 8055 that are referenced in the proof each make use of Regularity for their derivations. (The reverse implication can be derived without using Regularity; see dfac2a 8531.) TODO: Fix label in comment, and put label changes into list at top of set.mm. (Contributed by NM, 5-Apr-2004.) (Revised by Mario Carneiro, 26-Jun-2015.)
Assertion
Ref Expression
dfac2
Distinct variable group:   , , , ,

Proof of Theorem dfac2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfac3 8523 . . 3
2 nfra1 2838 . . . . . . 7
3 rsp 2823 . . . . . . . . . . . . 13
4 equid 1791 . . . . . . . . . . . . . . . . . . 19
5 neeq1 2738 . . . . . . . . . . . . . . . . . . . . 21
6 eqeq1 2461 . . . . . . . . . . . . . . . . . . . . 21
75, 6anbi12d 710 . . . . . . . . . . . . . . . . . . . 20
87rspcev 3210 . . . . . . . . . . . . . . . . . . 19
94, 8mpanr2 684 . . . . . . . . . . . . . . . . . 18
10 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . 22
1110preq1d 4115 . . . . . . . . . . . . . . . . . . . . 21
12 preq2 4110 . . . . . . . . . . . . . . . . . . . . 21
1311, 12eqtr2d 2499 . . . . . . . . . . . . . . . . . . . 20
1413anim2i 569 . . . . . . . . . . . . . . . . . . 19
1514reximi 2925 . . . . . . . . . . . . . . . . . 18
169, 15syl 16 . . . . . . . . . . . . . . . . 17
17 prex 4694 . . . . . . . . . . . . . . . . . 18
18 eqeq1 2461 . . . . . . . . . . . . . . . . . . . 20
1918anbi2d 703 . . . . . . . . . . . . . . . . . . 19
2019rexbidv 2968 . . . . . . . . . . . . . . . . . 18
2117, 20elab 3246 . . . . . . . . . . . . . . . . 17
2216, 21sylibr 212 . . . . . . . . . . . . . . . 16
23 vex 3112 . . . . . . . . . . . . . . . . . 18
2423prid2 4139 . . . . . . . . . . . . . . . . 17
25 fvex 5881 . . . . . . . . . . . . . . . . . 18
2625prid1 4138 . . . . . . . . . . . . . . . . 17
2724, 26pm3.2i 455 . . . . . . . . . . . . . . . 16
28 eleq2 2530 . . . . . . . . . . . . . . . . . 18
29 eleq2 2530 . . . . . . . . . . . . . . . . . 18
3028, 29anbi12d 710 . . . . . . . . . . . . . . . . 17
3130rspcev 3210 . . . . . . . . . . . . . . . 16
3222, 27, 31sylancl 662 . . . . . . . . . . . . . . 15
33 eleq1 2529 . . . . . . . . . . . . . . . . 17
34 eleq1 2529 . . . . . . . . . . . . . . . . . . 19
3534anbi2d 703 . . . . . . . . . . . . . . . . . 18
3635rexbidv 2968 . . . . . . . . . . . . . . . . 17
3733, 36anbi12d 710 . . . . . . . . . . . . . . . 16
3825, 37spcev 3201 . . . . . . . . . . . . . . 15
3932, 38sylan2 474 . . . . . . . . . . . . . 14
4039ex 434 . . . . . . . . . . . . 13
413, 40syl8 70 . . . . . . . . . . . 12
4241impd 431 . . . . . . . . . . 11
4342pm2.43d 48 . . . . . . . . . 10
44 df-rex 2813 . . . . . . . . . . . . . 14
45 vex 3112 . . . . . . . . . . . . . . . . . . . 20
46 eqeq1 2461 . . . . . . . . . . . . . . . . . . . . . 22
4746anbi2d 703 . . . . . . . . . . . . . . . . . . . . 21
4847rexbidv 2968 . . . . . . . . . . . . . . . . . . . 20
4945, 48elab 3246 . . . . . . . . . . . . . . . . . . 19
50 neeq1 2738 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
51 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
5251eleq1d 2526 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
53 eleq2 2530 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
5452, 53bitrd 253 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
5550, 54imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . 26
5655rspccv 3207 . . . . . . . . . . . . . . . . . . . . . . . . 25
57 elirrv 8044 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
58 eleq2 2530 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
5957, 58mtbii 302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
6059con2i 120 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
61 vex 3112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
62 fvex 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
63 vex 3112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
6461, 23, 62, 63prel12 4207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
65 ancom 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
66 eleq2 2530 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
67 eleq2 2530 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
6866, 67anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
6965, 68syl5rbbr 260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
7064, 69sylan9bbr 700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
7160, 70sylan2 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
7271adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
7372pm5.32da 641 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
7461, 23, 62, 63preleq 8055 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
7573, 74syl6bir 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7651eqeq2d 2471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
7776biimparc 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7875, 77syl6 33 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
7978exp4c 608 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8079com13 80 . . . . . . . . . . . . . . . . . . . . . . . . 25
8156, 80syl8 70 . . . . . . . . . . . . . . . . . . . . . . . 24
8281com4r 86 . . . . . . . . . . . . . . . . . . . . . . 23
8382imp 429 . . . . . . . . . . . . . . . . . . . . . 22
8483imp4a 589 . . . . . . . . . . . . . . . . . . . . 21
8584com3l 81 . . . . . . . . . . . . . . . . . . . 20
8685rexlimiv 2943 . . . . . . . . . . . . . . . . . . 19
8749, 86sylbi 195 . . . . . . . . . . . . . . . . . 18
8887expd 436 . . . . . . . . . . . . . . . . 17
8988com13 80 . . . . . . . . . . . . . . . 16
9089imp4b 590 . . . . . . . . . . . . . . 15
9190exlimdv 1724 . . . . . . . . . . . . . 14
9244, 91syl5bi 217 . . . . . . . . . . . . 13
9392expimpd 603 . . . . . . . . . . . 12
9493alrimiv 1719 . . . . . . . . . . 11
95 mo2icl 3278 . . . . . . . . . . 11
9694, 95syl 16 . . . . . . . . . 10
9743, 96jctird 544 . . . . . . . . 9
98 df-reu 2814 . . . . . . . . . 10
99 eu5 2310 . . . . . . . . . 10
10098, 99bitri 249 . . . . . . . . 9
10197, 100syl6ibr 227 . . . . . . . 8
102101expd 436 . . . . . . 7
1032, 102ralrimi 2857 . . . . . 6
104 vex 3112 . . . . . . . . . . . 12
105104rnex 6734 . . . . . . . . . . 11
106 p0ex 4639 . . . . . . . . . . 11
107105, 106unex 6598 . . . . . . . . . 10
108 vex 3112 . . . . . . . . . 10
109107, 108unex 6598 . . . . . . . . 9
110109pwex 4635 . . . . . . . 8
111 ssun1 3666 . . . . . . . . . . . . . . 15
112 fvrn0 5893 . . . . . . . . . . . . . . 15
113111, 112sselii 3500 . . . . . . . . . . . . . 14
114 elun2 3671 . . . . . . . . . . . . . 14
115 prssi 4186 . . . . . . . . . . . . . 14
116113, 114, 115sylancr 663 . . . . . . . . . . . . 13
117 prex 4694 . . . . . . . . . . . . . 14
118117elpw 4018 . . . . . . . . . . . . 13
119116, 118sylibr 212 . . . . . . . . . . . 12
120 eleq1 2529 . . . . . . . . . . . 12
121119, 120syl5ibrcom 222 . . . . . . . . . . 11
122121adantld 467 . . . . . . . . . 10
123122rexlimiv 2943 . . . . . . . . 9
124123abssi 3574 . . . . . . . 8
125110, 124ssexi 4597 . . . . . . 7
126 rexeq 3055 . . . . . . . . . 10
127126reubidv 3042 . . . . . . . . 9
128127imbi2d 316 . . . . . . . 8
129128ralbidv 2896 . . . . . . 7
130125, 129spcev 3201 . . . . . 6
131103, 130syl 16 . . . . 5
132131exlimiv 1722 . . . 4
133132alimi 1633 . . 3
1341, 133sylbi 195 . 2
135 dfac2a 8531 . 2
136134, 135impbii 188 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  =wceq 1395  E.wex 1612  e.wcel 1818  E!weu 2282  E*wmo 2283  {cab 2442  =/=wne 2652  A.wral 2807  E.wrex 2808  E!wreu 2809  u.cun 3473  C_wss 3475   c0 3784  ~Pcpw 4012  {csn 4029  {cpr 4031  rancrn 5005  `cfv 5593   wac 8517
This theorem is referenced by:  dfac7  8533
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  ax-reg 8039
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  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-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-eprel 4796  df-id 4800  df-fr 4843  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-fv 5601  df-riota 6257  df-ac 8518
  Copyright terms: Public domain W3C validator