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

Theorem zorn 7590
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 7589 for a version with general partial orderings. (Contributed by NM, 12-Aug-2004.)
Hypothesis
Ref Expression
zornn0.1  |-  A  e.  _V
Assertion
Ref Expression
zorn  |-  ( A. z ( ( z 
C_  A  /\ [ C_]  Or  z )  ->  U. z  e.  A )  ->  E. x  e.  A  A. y  e.  A  -.  x  C.  y )
Distinct variable group:    x, y, z, A

Proof of Theorem zorn
StepHypRef Expression
1 zornn0.1 . . 3  |-  A  e.  _V
2 numth3 7535 . . 3  |-  ( A  e.  _V  ->  A  e.  dom  card )
31, 2ax-mp 8 . 2  |-  A  e.  dom  card
4 zorng 7587 . 2  |-  ( ( A  e.  dom  card  /\  A. z ( ( z 
C_  A  /\ [ C_]  Or  z )  ->  U. z  e.  A ) )  ->  E. x  e.  A  A. y  e.  A  -.  x  C.  y )
53, 4mpan 647 1  |-  ( A. z ( ( z 
C_  A  /\ [ C_]  Or  z )  ->  U. z  e.  A )  ->  E. x  e.  A  A. y  e.  A  -.  x  C.  y )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 357   A.wal 1450    e. wcel 1538   A.wral 2291   E.wrex 2292   _Vcvv 2492    C_ wss 2810    C. wpss 2811   U.cuni 3438    Or wor 3878   dom cdm 4275   [ C_] crpss 5747   cardccrd 7030
This theorem is referenced by:  alexsubALTlem2  15466
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1451  ax-6 1452  ax-7 1453  ax-gen 1454  ax-8 1540  ax-11 1541  ax-13 1542  ax-14 1543  ax-17 1545  ax-12o 1578  ax-10 1592  ax-9 1598  ax-4 1606  ax-16 1793  ax-ext 2064  ax-rep 3705  ax-sep 3715  ax-nul 3723  ax-pow 3759  ax-pr 3783  ax-un 4075  ax-ac 7528
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 904  df-3an 905  df-ex 1456  df-sb 1754  df-eu 1976  df-mo 1977  df-clab 2070  df-cleq 2075  df-clel 2078  df-ne 2201  df-ral 2295  df-rex 2296  df-reu 2297  df-rab 2298  df-v 2494  df-sbc 2668  df-csb 2750  df-dif 2813  df-un 2815  df-in 2817  df-ss 2821  df-pss 2823  df-nul 3089  df-if 3199  df-pw 3260  df-sn 3278  df-pr 3279  df-tp 3280  df-op 3281  df-uni 3439  df-int 3473  df-iun 3516  df-br 3601  df-opab 3655  df-mpt 3656  df-tr 3688  df-eprel 3870  df-id 3874  df-po 3879  df-so 3880  df-fr 3917  df-se 3918  df-we 3919  df-ord 3960  df-on 3961  df-suc 3963  df-xp 4289  df-rel 4290  df-cnv 4291  df-co 4292  df-dm 4293  df-rn 4294  df-res 4295  df-ima 4296  df-fun 4297  df-fn 4298  df-f 4299  df-f1 4300  df-fo 4301  df-f1o 4302  df-fv 4303  df-iso 4304  df-rpss 5748  df-iota 5762  df-recs 5835  df-en 6289  df-riota 6455  df-card 7034  df-ac 7203
Copyright terms: Public domain