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

Theorem zorn 6720
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 6719 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 2747 . . . . . . . 8
2 zornlem 6718 . . . . . . . 8
31, 2mtbir 288 . . . . . . 7
4 zornlem 6718 . . . . . . . 8
5 zornlem 6718 . . . . . . . 8
6 psstr 2751 . . . . . . . . 9
7 zornlem 6718 . . . . . . . . 9
86, 7sylibr 201 . . . . . . . 8
94, 5, 8syl2anb 458 . . . . . . 7
103, 9pm3.2i 434 . . . . . 6
1110a1i 10 . . . . 5
1211rgen3 2215 . . . 4
13 df-po 3642 . . . 4
1412, 13mpbir 198 . . 3
15 df-so 3656 . . . . . . . 8
1615simprbi 443 . . . . . . 7
17 zornlem 6718 . . . . . . . . . 10
18 biid 225 . . . . . . . . . 10
1917, 18, 53orbi123i 1102 . . . . . . . . 9
20 sspsstri 2749 . . . . . . . . 9
2119, 20bitr4i 241 . . . . . . . 8
22212ralbii 2151 . . . . . . 7
2316, 22sylib 186 . . . . . 6
2423anim2i 546 . . . . 5
25 risset 2167 . . . . . 6
26 eqimss2 2708 . . . . . . . . 9
27 unissb 3261 . . . . . . . . 9
2826, 27sylib 186 . . . . . . . 8
297orbi1i 501 . . . . . . . . . 10
30 sspss 2746 . . . . . . . . . 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 6719 . . 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 2326   wss 2636   wpss 2637  cuni 3233   class class class wbr 3383  copab 3437   wpo 3640   wor 3641
This theorem is referenced by:  zornn0 6721  alexsublem2 12127
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 3469  ax-sep 3479  ax-nul 3488  ax-pow 3524  ax-pr 3548  ax-un 3823  ax-ac 6664
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 2328  df-sbc 2495  df-csb 2577  df-dif 2639  df-un 2641  df-in 2643  df-ss 2647  df-pss 2649  df-nul 2905  df-pw 3072  df-sn 3089  df-pr 3090  df-tp 3091  df-op 3092  df-uni 3234  df-int 3268  df-iun 3307  df-br 3384  df-opab 3438  df-tr 3453  df-eprel 3634  df-id 3637  df-po 3642  df-so 3656  df-fr 3676  df-we 3692  df-ord 3708  df-on 3709  df-suc 3711  df-xp 4035  df-rel 4036  df-cnv 4037  df-co 4038  df-dm 4039  df-rn 4040  df-res 4041  df-ima 4042  df-fun 4043  df-fn 4044  df-f 4045  df-f1 4046  df-fo 4047  df-f1o 4048  df-fv 4049  df-iso 4050  df-en 5830
Copyright terms: Public domain