zorn - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem zorn 4721

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 4720 for a version with general partial orderings.

**Hypothesis**
Ref	Expression
zorn2.1

**Assertion**
Ref	Expression
zorn	$/\$ $\/$

Distinct variable group:

**Proof of Theorem zorn**
Step	Hyp	Ref	Expression
1		df-so 2814	. . . . . . . 8 $/\$ $\/$ $\/$
2	1	pm3.27bi 326	. . . . . . 7 $\/$ $\/$
3		zornlem 4719	. . . . . . . . . 10
4		pm4.2 170	. . . . . . . . . 10
5		zornlem 4719	. . . . . . . . . 10
6	3, 4, 5	3orbi123i 820	. . . . . . . . 9 $\/$ $\/$ $\/$ $\/$
7		sspsstri 2119	. . . . . . . . 9 $\/$ $\/$ $\/$
8	6, 7	bitr4 176	. . . . . . . 8 $\/$ $\/$ $\/$
9	8	2ralbii 1645	. . . . . . 7 $\/$ $\/$ $\/$
10	2, 9	sylib 198	. . . . . 6 $\/$
11	10	anim2i 335	. . . . 5 $/\$ $/\$ $\/$
12		risset 1661	. . . . . 6
13		eqimss2 2081	. . . . . . . . 9
14		unissb 2496	. . . . . . . . 9
15	13, 14	sylib 198	. . . . . . . 8
16		zornlem 4719	. . . . . . . . . . 11
17	16	orbi1i 256	. . . . . . . . . 10 $\/$ $\/$
18		sspss 2116	. . . . . . . . . 10 $\/$
19	17, 18	bitr4 176	. . . . . . . . 9 $\/$
20	19	ralbii 1643	. . . . . . . 8 $\/$
21	15, 20	sylibr 200	. . . . . . 7 $\/$
22	21	r19.22si 1710	. . . . . 6 $\/$
23	12, 22	sylbi 199	. . . . 5 $\/$
24	11, 23	imim12i 18	. . . 4 $/\$ $\/$ $/\$ $\/$
25	24	19.20i 968	. . 3 $/\$ $\/$ $/\$ $\/$
26		pssirr 2117	. . . . . . . . 9
27		zornlem 4719	. . . . . . . . 9
28	26, 27	mtbir 192	. . . . . . . 8
29		psstr 2121	. . . . . . . . . 10 $/\$
30	29, 16	sylibr 200	. . . . . . . . 9 $/\$
31		zornlem 4719	. . . . . . . . 9
32	30, 31, 5	syl2anb 455	. . . . . . . 8 $/\$
33	28, 32	pm3.2i 285	. . . . . . 7 $/\$ $/\$
34	33	a1i 8	. . . . . 6 $/\$ $/\$ $/\$ $/\$
35	34	rgen3 1700	. . . . 5 $/\$ $/\$
36		df-po 2804	. . . . 5 $/\$ $/\$
37	35, 36	mpbir 190	. . . 4
38		zorn2.1	. . . . 5
39	38	zorn2 4720	. . . 4 $/\$ $/\$ $\/$
40	37, 39	mpan 692	. . 3 $/\$ $\/$
41	25, 40	syl 10	. 2 $/\$ $\/$
42	3	negbii 187	. . . 4
43	42	ralbii 1643	. . 3
44	43	rexbii 1644	. 2
45	41, 44	sylib 198	1 $/\$ $\/$

Colors of variables: wff set class

Syntax hints:

wn 2

wi 3 $\/$ wo 222 $/\$ wa 223 $\/$ w3o 771 $/\$ w3a 772

wal 950

wceq 1099

wcel 1105

wral 1621

wrex 1622

cvv 1786

wss 2018

wpss 2019

cuni 2471 class class class wbr 2587

copab 2634

wpo 2802

wor 2803

This theorem is referenced by: infxpidmlem9 7454

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-4 951 ax-5 952 ax-6 953 ax-7 954 ax-gen 955 ax-8 1101 ax-9 1102 ax-10 1103 ax-12 1104 ax-13 1107 ax-14 1108 ax-11 1180 ax-17 1190 ax-16 1194 ax-11o 1202 ax-ext 1436 ax-rep 2661 ax-sep 2671 ax-nul 2678 ax-pow 2710 ax-pr 2747 ax-un 2830 ax-ac 4668

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 773 df-3an 774 df-ex 957 df-sb 1155 df-eu 1359 df-mo 1360 df-clab 1441 df-cleq 1446 df-clel 1449 df-ne 1563 df-ral 1625 df-rex 1626 df-reu 1627 df-rab 1628 df-v 1787 df-sbc 1913 df-dif 2020 df-un 2021 df-in 2022 df-ss 2024 df-pss 2026 df-nul 2252 df-pw 2373 df-sn 2383 df-pr 2384 df-tp 2386 df-op 2387 df-uni 2472 df-int 2502 df-iun 2536 df-br 2588 df-opab 2635 df-tr 2649 df-eprel 2794 df-id 2797 df-po 2804 df-so 2814 df-fr 2880 df-we 2897 df-ord 2914 df-on 2915 df-suc 2917 df-xp 3147 df-rel 3148 df-cnv 3149 df-co 3150 df-dm 3151 df-rn 3152 df-res 3153 df-ima 3154 df-fun 3155 df-fn 3156 df-f 3157 df-f1 3158 df-fo 3159 df-f1o 3160 df-fv 3161 df-iso 3162