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

Theorem konigth 8398
 Description: Konig's Theorem. If for all , then , where the sums and products stand in for disjoint union and infinite cartesian product. The version here is proven with regular unions rather than disjoint unions for convenience, but the version with disjoint unions is clearly a special case of this version. The Axiom of Choice is needed for this proof, but it contains AC as a simple corollary (letting , this theorem says that an infinite cartesian product of nonempty sets is nonempty), so this is an AC equivalent. Theorem 11.26 of [TakeutiZaring] p. 107. (Contributed by Mario Carneiro, 22-Feb-2013.)
Hypotheses
Ref Expression
konigth.1
konigth.2
konigth.3
Assertion
Ref Expression
konigth
Distinct variable group:   ,
Allowed substitution hints:   ()   ()   ()   ()

Proof of Theorem konigth
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 konigth.1 . 2
2 konigth.2 . 2
3 konigth.3 . 2
4 fveq2 5685 . . . . 5
54fveq1d 5687 . . . 4
65cbvmptv 4258 . . 3
76mpteq2i 4250 . 2
8 fveq2 5685 . . 3
98cbvmptv 4258 . 2
101, 2, 3, 7, 9konigthlem 8397 1
 Colors of variables: wff set class Syntax hints:   wi 4   wceq 1649   wcel 1721  wral 2664  cvv 2914  ciun 4051   class class class wbr 4170   cmpt 4224  cfv 5411  cixp 7020   csdm 7065 This theorem is referenced by:  pwcfsdom  8412 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2383  ax-rep 4278  ax-sep 4288  ax-nul 4296  ax-pow 4335  ax-pr 4361  ax-un 4658  ax-ac2 8297 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2256  df-mo 2257  df-clab 2389  df-cleq 2395  df-clel 2398  df-nfc 2527  df-ne 2567  df-ral 2669  df-rex 2670  df-reu 2671  df-rmo 2672  df-rab 2673  df-v 2916  df-sbc 3120  df-csb 3210  df-dif 3281  df-un 3283  df-in 3285  df-ss 3292  df-pss 3294  df-nul 3587  df-if 3698  df-pw 3759  df-sn 3778  df-pr 3779  df-tp 3780  df-op 3781  df-uni 3974  df-int 4009  df-iun 4053  df-br 4171  df-opab 4225  df-mpt 4226  df-tr 4261  df-eprel 4452  df-id 4456  df-po 4461  df-so 4462  df-fr 4499  df-se 4500  df-we 4501  df-ord 4542  df-on 4543  df-suc 4545  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5375  df-fun 5413  df-fn 5414  df-f 5415  df-f1 5416  df-fo 5417  df-f1o 5418  df-fv 5419  df-isom 5420  df-ov 6041  df-oprab 6042  df-mpt2 6043  df-1st 6306  df-2nd 6307  df-riota 6506  df-recs 6590  df-er 6862  df-map 6977  df-ixp 7021  df-en 7067  df-dom 7068  df-sdom 7069  df-card 7780  df-acn 7783  df-ac 7951
 Copyright terms: Public domain W3C validator