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

Theorem zorn 6780
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 6779 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 2750 . . . . . . . 8
2 zornlem 6778 . . . . . . . 8
31, 2mtbir 288 . . . . . . 7
4 zornlem 6778 . . . . . . . 8
5 zornlem 6778 . . . . . . . 8
6 psstr 2754 . . . . . . . . 9
7 zornlem 6778 . . . . . . . . 9
86, 7sylibr 201 . . . . . . . 8
94, 5, 8syl2anb 458 . . . . . . 7
103, 9pm3.2i 434 . . . . . 6
1110a1i 10 . . . . 5
1211rgen3 2215 . . . 4
13 df-po 3655 . . . 4
1412, 13mpbir 198 . . 3
15 df-so 3669 . . . . . . . 8
1615simprbi 443 . . . . . . 7
17 zornlem 6778 . . . . . . . . . 10
18 biid 225 . . . . . . . . . 10
1917, 18, 53orbi123i 1102 . . . . . . . . 9
20 sspsstri 2752 . . . . . . . . 9
2119, 20bitr4i 241 . . . . . . . 8
22212ralbii 2151 . . . . . . 7
2316, 22sylib 186 . . . . . 6
2423anim2i 546 . . . . 5
25 risset 2167 . . . . . 6
26 eqimss2 2709 . . . . . . . . 9
27 unissb 3274 . . . . . . . . 9
2826, 27sylib 186 . . . . . . . 8
297orbi1i 501 . . . . . . . . . 10
30 sspss 2749 . . . . . . . . . 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 6779 . . 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 2327   wss 2637   wpss 2638  cuni 3246   class class class wbr 3396  copab 3449   wpo 3653   wor 3654
This theorem is referenced by:  zornn0 6781  alexsublem2 12381
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 3481  ax-sep 3491  ax-nul 3500  ax-pow 3536  ax-pr 3560  ax-un 3836  ax-ac 6722
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 2329  df-sbc 2496  df-csb 2578  df-dif 2640  df-un 2642  df-in 2644  df-ss 2648  df-pss 2650  df-nul 2908  df-if 3015  df-pw 3075  df-sn 3092  df-pr 3093  df-tp 3094  df-op 3095  df-uni 3247  df-int 3281  df-iun 3320  df-br 3397  df-opab 3450  df-tr 3465  df-eprel 3646  df-id 3650  df-po 3655  df-so 3669  df-fr 3689  df-we 3705  df-ord 3721  df-on 3722  df-suc 3724  df-xp 4048  df-rel 4049  df-cnv 4050  df-co 4051  df-dm 4052  df-rn 4053  df-res 4054  df-ima 4055  df-fun 4056  df-fn 4057  df-f 4058  df-f1 4059  df-fo 4060  df-f1o 4061  df-fv 4062  df-iso 4063  df-mpt 5196  df-en 5869  df-card 6455
Copyright terms: Public domain