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

Theorem zorn 6513
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 6512 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 2743 . . . . . . . 8
2 zornlem 6511 . . . . . . . 8
31, 2mtbir 290 . . . . . . 7
4 zornlem 6511 . . . . . . . 8
5 zornlem 6511 . . . . . . . 8
6 psstr 2747 . . . . . . . . 9
7 zornlem 6511 . . . . . . . . 9
86, 7sylibr 201 . . . . . . . 8
94, 5, 8syl2anb 462 . . . . . . 7
103, 9pm3.2i 438 . . . . . 6
1110a1i 10 . . . . 5
1211rgen3 2226 . . . 4
13 df-po 3616 . . . 4
1412, 13mpbir 198 . . 3
15 df-so 3630 . . . . . . . 8
1615simprbi 447 . . . . . . 7
17 zornlem 6511 . . . . . . . . . 10
18 biid 226 . . . . . . . . . 10
1917, 18, 53orbi123i 1113 . . . . . . . . 9
20 sspsstri 2745 . . . . . . . . 9
2119, 20bitr4i 242 . . . . . . . 8
22212ralbii 2162 . . . . . . 7
2316, 22sylib 186 . . . . . 6
2423anim2i 550 . . . . 5
25 risset 2178 . . . . . 6
26 eqimss2 2706 . . . . . . . . 9
27 unissb 3241 . . . . . . . . 9
2826, 27sylib 186 . . . . . . . 8
297orbi1i 505 . . . . . . . . . 10
30 sspss 2742 . . . . . . . . . 10
3129, 30bitr4i 242 . . . . . . . . 9
3231ralbii 2160 . . . . . . . 8
3328, 32sylibr 201 . . . . . . 7
3433reximi 2236 . . . . . 6
3525, 34sylbi 185 . . . . 5
3624, 35imim12i 52 . . . 4
3736alimi 1353 . . 3
38 zorn2.1 . . . 4
3938zorn2 6512 . . 3
4014, 37, 39sylancr 643 . 2
4117notbii 287 . . . 4
4241ralbii 2160 . . 3
4342rexbii 2161 . 2
4440, 43sylib 186 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wo 359   wa 360   w3o 911   w3a 912  wal 1341   wceq 1425   wcel 1427  wral 2138  wrex 2139  cvv 2335   wss 2634   wpss 2635  cuni 3213   class class class wbr 3358  copab 3412   wpo 3614   wor 3615
This theorem is referenced by:  zornn0 6514  alexsublem2 16919
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1342  ax-6 1343  ax-7 1344  ax-gen 1345  ax-8 1429  ax-10 1430  ax-11 1431  ax-12 1432  ax-13 1433  ax-14 1434  ax-17 1441  ax-9 1456  ax-4 1462  ax-16 1640  ax-ext 1911  ax-rep 3444  ax-sep 3454  ax-nul 3463  ax-pow 3499  ax-pr 3523  ax-un 3795  ax-ac 6456
This theorem depends on definitions:  df-bi 175  df-or 361  df-an 362  df-3or 913  df-3an 914  df-ex 1347  df-sb 1602  df-eu 1829  df-mo 1830  df-clab 1917  df-cleq 1922  df-clel 1925  df-ne 2049  df-ral 2142  df-rex 2143  df-reu 2144  df-rab 2145  df-v 2337  df-sbc 2502  df-csb 2577  df-dif 2637  df-un 2639  df-in 2641  df-ss 2643  df-pss 2645  df-nul 2900  df-pw 3063  df-sn 3080  df-pr 3081  df-tp 3082  df-op 3083  df-uni 3214  df-int 3248  df-iun 3286  df-br 3359  df-opab 3413  df-tr 3428  df-eprel 3608  df-id 3611  df-po 3616  df-so 3630  df-fr 3649  df-we 3665  df-ord 3681  df-on 3682  df-suc 3684  df-xp 4005  df-rel 4006  df-cnv 4007  df-co 4008  df-dm 4009  df-rn 4010  df-res 4011  df-ima 4012  df-fun 4013  df-fn 4014  df-f 4015  df-f1 4016  df-fo 4017  df-f1o 4018  df-fv 4019  df-iso 4020  df-en 5682
Copyright terms: Public domain