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

Theorem zorn 6615
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 6614 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 2741 . . . . . . . 8
2 zornlem 6613 . . . . . . . 8
31, 2mtbir 287 . . . . . . 7
4 zornlem 6613 . . . . . . . 8
5 zornlem 6613 . . . . . . . 8
6 psstr 2745 . . . . . . . . 9
7 zornlem 6613 . . . . . . . . 9
86, 7sylibr 200 . . . . . . . 8
94, 5, 8syl2anb 457 . . . . . . 7
103, 9pm3.2i 433 . . . . . 6
1110a1i 10 . . . . 5
1211rgen3 2213 . . . 4
13 df-po 3616 . . . 4
1412, 13mpbir 197 . . 3
15 df-so 3630 . . . . . . . 8
1615simprbi 442 . . . . . . 7
17 zornlem 6613 . . . . . . . . . 10
18 biid 224 . . . . . . . . . 10
1917, 18, 53orbi123i 1101 . . . . . . . . 9
20 sspsstri 2743 . . . . . . . . 9
2119, 20bitr4i 240 . . . . . . . 8
22212ralbii 2149 . . . . . . 7
2316, 22sylib 185 . . . . . 6
2423anim2i 545 . . . . 5
25 risset 2165 . . . . . 6
26 eqimss2 2704 . . . . . . . . 9
27 unissb 3241 . . . . . . . . 9
2826, 27sylib 185 . . . . . . . 8
297orbi1i 500 . . . . . . . . . 10
30 sspss 2740 . . . . . . . . . 10
3129, 30bitr4i 240 . . . . . . . . 9
3231ralbii 2147 . . . . . . . 8
3328, 32sylibr 200 . . . . . . 7
3433reximi 2223 . . . . . 6
3525, 34sylbi 184 . . . . 5
3624, 35imim12i 52 . . . 4
3736alimi 1341 . . 3
38 zorn2.1 . . . 4
3938zorn2 6614 . . 3
4014, 37, 39sylancr 638 . 2
4117notbii 284 . . . 4
4241ralbii 2147 . . 3
4342rexbii 2148 . 2
4440, 43sylib 185 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wo 355   wa 356   w3o 897   w3a 898  wal 1329   wceq 1413   wcel 1415  wral 2125  wrex 2126  cvv 2322   wss 2632   wpss 2633  cuni 3213   class class class wbr 3358  copab 3412   wpo 3614   wor 3615
This theorem is referenced by:  zornn0 6616  alexsublem2 17835
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1330  ax-6 1331  ax-7 1332  ax-gen 1333  ax-8 1417  ax-10 1418  ax-11 1419  ax-12 1420  ax-13 1421  ax-14 1422  ax-17 1429  ax-9 1444  ax-4 1450  ax-16 1628  ax-ext 1899  ax-rep 3444  ax-sep 3454  ax-nul 3463  ax-pow 3499  ax-pr 3523  ax-un 3797  ax-ac 6559
This theorem depends on definitions:  df-bi 174  df-or 357  df-an 358  df-3or 899  df-3an 900  df-ex 1335  df-sb 1590  df-eu 1817  df-mo 1818  df-clab 1905  df-cleq 1910  df-clel 1913  df-ne 2036  df-ral 2129  df-rex 2130  df-reu 2131  df-rab 2132  df-v 2324  df-sbc 2491  df-csb 2573  df-dif 2635  df-un 2637  df-in 2639  df-ss 2641  df-pss 2643  df-nul 2899  df-pw 3062  df-sn 3079  df-pr 3080  df-tp 3081  df-op 3082  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 3650  df-we 3666  df-ord 3682  df-on 3683  df-suc 3685  df-xp 4009  df-rel 4010  df-cnv 4011  df-co 4012  df-dm 4013  df-rn 4014  df-res 4015  df-ima 4016  df-fun 4017  df-fn 4018  df-f 4019  df-f1 4020  df-fo 4021  df-f1o 4022  df-fv 4023  df-iso 4024  df-en 5750
Copyright terms: Public domain