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

Theorem zorn 6444
 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 6443 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 2964 . . . . . . . 8
2 zornlem 6442 . . . . . . . 8
31, 2mtbir 367 . . . . . . 7
4 zornlem 6442 . . . . . . . 8
5 zornlem 6442 . . . . . . . 8
6 psstr 2968 . . . . . . . . 9
7 zornlem 6442 . . . . . . . . 9
86, 7sylibr 264 . . . . . . . 8
94, 5, 8syl2anb 700 . . . . . . 7
103, 9pm3.2i 514 . . . . . 6
1110a1i 8 . . . . 5
1211rgen3 2468 . . . 4
13 df-po 3784 . . . 4
1412, 13mpbir 255 . . 3
15 df-so 3796 . . . . . . . 8
1615simprbi 542 . . . . . . 7
17 zornlem 6442 . . . . . . . . . 10
18 biid 289 . . . . . . . . . 10
1917, 18, 53orbi123i 1335 . . . . . . . . 9
20 sspsstri 2966 . . . . . . . . 9
2119, 20bitr4i 310 . . . . . . . 8
22212ralbii 2409 . . . . . . 7
2316, 22sylib 263 . . . . . 6
2423anim2i 635 . . . . 5
25 risset 2425 . . . . . 6
26 eqimss2 2927 . . . . . . . . 9
27 unissb 3426 . . . . . . . . 9
2826, 27sylib 263 . . . . . . . 8
297orbi1i 574 . . . . . . . . . 10
30 sspss 2963 . . . . . . . . . 10
3129, 30bitr4i 310 . . . . . . . . 9
3231ralbii 2407 . . . . . . . 8
3328, 32sylibr 264 . . . . . . 7
3433reximi 2478 . . . . . 6
3525, 34sylbi 237 . . . . 5
3624, 35imim12i 35 . . . 4
3736alimi 1656 . . 3
38 zorn2.1 . . . 4
3938zorn2 6443 . . 3
4014, 37, 39sylancr 758 . 2
4117notbii 362 . . . 4
4241ralbii 2407 . . 3
4342rexbii 2408 . 2
4440, 43sylib 263 1
 Colors of variables: wff set class Syntax hints:   wn 2   wi 3   wo 432   wa 433   w3o 1129   w3a 1130  wal 1613   wceq 1615   wcel 1617  wral 2385  wrex 2386  cvv 2569   wss 2859   wpss 2860  cuni 3398   class class class wbr 3539  copab 3597   wpo 3782   wor 3783 This theorem is referenced by:  infxpidmlem9OLD 9359  alexsublem2 16523  filssufil 16656  zornn0 16849 This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-13 1628  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-rep 3628  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719  ax-un 3961  ax-ac 6385 This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3or 1131  df-3an 1132  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-ral 2389  df-rex 2390  df-reu 2391  df-rab 2392  df-v 2571  df-sbc 2731  df-csb 2806  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-pss 2870  df-nul 3115  df-pw 3261  df-sn 3274  df-pr 3275  df-tp 3277  df-op 3278  df-uni 3399  df-int 3433  df-iun 3470  df-br 3540  df-opab 3598  df-tr 3612  df-eprel 3776  df-id 3779  df-po 3784  df-so 3796  df-fr 3814  df-we 3830  df-ord 3846  df-on 3847  df-suc 3849  df-xp 4165  df-rel 4166  df-cnv 4167  df-co 4168  df-dm 4169  df-rn 4170  df-res 4171  df-ima 4172  df-fun 4173  df-fn 4174  df-f 4175  df-f1 4176  df-fo 4177  df-f1o 4178  df-fv 4179  df-iso 4180  df-en 5631
Copyright terms: Public domain