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

Theorem zorn 6678
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 6677 for a version with general partial orderings.
Hypothesis
Ref Expression
zorn2.1
Assertion
Ref Expression
zorn
Distinct variable group:   ,,,

Proof of Theorem zorn
StepHypRef Expression
1 pssirr 2745 . . . . . . . 8
2 zornlem 6676 . . . . . . . 8
31, 2mtbir 288 . . . . . . 7
4 zornlem 6676 . . . . . . . 8
5 zornlem 6676 . . . . . . . 8
6 psstr 2749 . . . . . . . . 9
7 zornlem 6676 . . . . . . . . 9
86, 7sylibr 201 . . . . . . . 8
94, 5, 8syl2anb 458 . . . . . . 7
103, 9pm3.2i 434 . . . . . 6
1110a1i 10 . . . . 5
1211rgen3 2215 . . . 4
13 df-po 3628 . . . 4
1412, 13mpbir 198 . . 3
15 df-so 3642 . . . . . . . 8
1615simprbi 443 . . . . . . 7
17 zornlem 6676 . . . . . . . . . 10
18 biid 225 . . . . . . . . . 10
1917, 18, 53orbi123i 1102 . . . . . . . . 9
20 sspsstri 2747 . . . . . . . . 9
2119, 20bitr4i 241 . . . . . . . 8
22212ralbii 2151 . . . . . . 7
2316, 22sylib 186 . . . . . 6
2423anim2i 546 . . . . 5
25 risset 2167 . . . . . 6
26 eqimss2 2706 . . . . . . . . 9
27 unissb 3251 . . . . . . . . 9
2826, 27sylib 186 . . . . . . . 8
297orbi1i 501 . . . . . . . . . 10
30 sspss 2744 . . . . . . . . . 10
3129, 30bitr4i 241 . . . . . . . . 9
3231ralbii 2149 . . . . . . . 8
3328, 32sylibr 201 . . . . . . 7
3433reximi 2225 . . . . . 6
3525, 34sylbi 185 . . . . 5
3624, 35imim12i 53 . . . 4
3736alimi 1342 . . 3
38 zorn2.1 . . . 4
3938zorn2 6677 . . 3
4014, 37, 39sylancr 639 . 2
4117notbii 285 . . . 4
4241ralbii 2149 . . 3
4342rexbii 2150 . 2
4440, 43sylib 186 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wo 356   wa 357   w3o 898   w3a 899  wal 1330   wceq 1414   wcel 1416  wral 2127  wrex 2128  cvv 2324   wss 2634   wpss 2635  cuni 3223   class class class wbr 3370  copab 3424   wpo 3626   wor 3627
This theorem is referenced by:  zornn0 6679  alexsublem2 11888
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1331  ax-6 1332  ax-7 1333  ax-gen 1334  ax-8 1418  ax-10 1419  ax-11 1420  ax-12 1421  ax-13 1422  ax-14 1423  ax-17 1430  ax-9 1445  ax-4 1451  ax-16 1629  ax-ext 1900  ax-rep 3456  ax-sep 3466  ax-nul 3475  ax-pow 3511  ax-pr 3535  ax-un 3809  ax-ac 6622
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 900  df-3an 901  df-ex 1336  df-sb 1591  df-eu 1818  df-mo 1819  df-clab 1906  df-cleq 1911  df-clel 1914  df-ne 2037  df-ral 2131  df-rex 2132  df-reu 2133  df-rab 2134  df-v 2326  df-sbc 2493  df-csb 2575  df-dif 2637  df-un 2639  df-in 2641  df-ss 2645  df-pss 2647  df-nul 2903  df-pw 3068  df-sn 3085  df-pr 3086  df-tp 3087  df-op 3088  df-uni 3224  df-int 3258  df-iun 3297  df-br 3371  df-opab 3425  df-tr 3440  df-eprel 3620  df-id 3623  df-po 3628  df-so 3642  df-fr 3662  df-we 3678  df-ord 3694  df-on 3695  df-suc 3697  df-xp 4021  df-rel 4022  df-cnv 4023  df-co 4024  df-dm 4025  df-rn 4026  df-res 4027  df-ima 4028  df-fun 4029  df-fn 4030  df-f 4031  df-f1 4032  df-fo 4033  df-f1o 4034  df-fv 4035  df-iso 4036  df-en 5800
Copyright terms: Public domain