HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem zorn 7515
Description: Zorn's Lemma. If the union of every chain (with respect to inclusion) in a set belongs to the set, then the set contains a maximal element. This theorem is equivalent to the Axiom of Choice. Theorem 6M of [Enderton] p. 151. See zorn2 7514 for a version with general partial orderings.
Hypothesis
Ref Expression
zornn0.1
Assertion
Ref Expression
zorn []
Distinct variable group:   ,,,

Proof of Theorem zorn
StepHypRef Expression
1 zornn0.1 . . 3
2 numth3 7499 . . 3
31, 2ax-mp 8 . 2
4 zorng 7512 . 2 []
53, 4mpan 646 1 []
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wa 357  wal 1445   wcel 1533  wral 2299  wrex 2300  cvv 2500   wss 2810   wpss 2811  cuni 3434   wor 3852   cdm 4249   [] crpss 5725  ccrd 6980
This theorem is referenced by:  alexsublem2  13818
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-7 1448  ax-gen 1449  ax-8 1535  ax-11 1536  ax-12 1537  ax-13 1538  ax-14 1539  ax-17 1542  ax-9 1563  ax-10 1591  ax-4 1605  ax-16 1790  ax-ext 2072  ax-rep 3677  ax-sep 3687  ax-nul 3696  ax-pow 3732  ax-pr 3756  ax-un 4049  ax-ac 7453
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 900  df-3an 901  df-ex 1451  df-sb 1751  df-eu 1984  df-mo 1985  df-clab 2078  df-cleq 2083  df-clel 2086  df-ne 2209  df-ral 2303  df-rex 2304  df-reu 2305  df-rab 2306  df-v 2502  df-sbc 2669  df-csb 2751  df-dif 2813  df-un 2815  df-in 2817  df-ss 2821  df-pss 2823  df-nul 3086  df-if 3195  df-pw 3256  df-sn 3274  df-pr 3275  df-tp 3276  df-op 3277  df-uni 3435  df-int 3469  df-iun 3511  df-br 3592  df-opab 3645  df-tr 3660  df-eprel 3844  df-id 3848  df-po 3853  df-so 3854  df-fr 3891  df-se 3892  df-we 3893  df-ord 3934  df-on 3935  df-suc 3937  df-xp 4263  df-rel 4264  df-cnv 4265  df-co 4266  df-dm 4267  df-rn 4268  df-res 4269  df-ima 4270  df-fun 4271  df-fn 4272  df-f 4273  df-f1 4274  df-fo 4275  df-f1o 4276  df-fv 4277  df-iso 4278  df-mpt 5461  df-rpss 5726  df-iota 5740  df-recs 5814  df-en 6249  df-riota 6415  df-card 6983  df-ac 7133
Copyright terms: Public domain