zorn - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem zorn 4807

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 4806 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 2856	. . . . . . . 8 $/\$ $\/$ $\/$
2	1	pm3.27bi 326	. . . . . . 7 $\/$ $\/$
3		zornlem 4805	. . . . . . . . . 10
4		pm4.2 170	. . . . . . . . . 10
5		zornlem 4805	. . . . . . . . . 10
6	3, 4, 5	3orbi123i 825	. . . . . . . . 9 $\/$ $\/$ $\/$ $\/$
7		sspsstri 2151	. . . . . . . . 9 $\/$ $\/$ $\/$
8	6, 7	bitr4 176	. . . . . . . 8 $\/$ $\/$ $\/$
9	8	2ralbii 1672	. . . . . . 7 $\/$ $\/$ $\/$
10	2, 9	sylib 198	. . . . . 6 $\/$
11	10	anim2i 335	. . . . 5 $/\$ $/\$ $\/$
12		risset 1688	. . . . . 6
13		eqimss2 2113	. . . . . . . . 9
14		unissb 2532	. . . . . . . . 9
15	13, 14	sylib 198	. . . . . . . 8
16		zornlem 4805	. . . . . . . . . . 11
17	16	orbi1i 256	. . . . . . . . . 10 $\/$ $\/$
18		sspss 2148	. . . . . . . . . 10 $\/$
19	17, 18	bitr4 176	. . . . . . . . 9 $\/$
20	19	ralbii 1670	. . . . . . . 8 $\/$
21	15, 20	sylibr 200	. . . . . . 7 $\/$
22	21	r19.22si 1737	. . . . . 6 $\/$
23	12, 22	sylbi 199	. . . . 5 $\/$
24	11, 23	imim12i 18	. . . 4 $/\$ $\/$ $/\$ $\/$
25	24	19.20i 994	. . 3 $/\$ $\/$ $/\$ $\/$
26		pssirr 2149	. . . . . . . . 9
27		zornlem 4805	. . . . . . . . 9
28	26, 27	mtbir 192	. . . . . . . 8
29		psstr 2153	. . . . . . . . . 10 $/\$
30	29, 16	sylibr 200	. . . . . . . . 9 $/\$
31		zornlem 4805	. . . . . . . . 9
32	30, 31, 5	syl2anb 457	. . . . . . . 8 $/\$
33	28, 32	pm3.2i 285	. . . . . . 7 $/\$ $/\$
34	33	a1i 8	. . . . . 6 $/\$ $/\$ $/\$ $/\$
35	34	rgen3 1727	. . . . 5 $/\$ $/\$
36		df-po 2846	. . . . 5 $/\$ $/\$
37	35, 36	mpbir 190	. . . 4
38		zorn2.1	. . . . 5
39	38	zorn2 4806	. . . 4 $/\$ $/\$ $\/$
40	37, 39	mpan 697	. . 3 $/\$ $\/$
41	25, 40	syl 10	. 2 $/\$ $\/$
42	3	negbii 187	. . . 4
43	42	ralbii 1670	. . 3
44	43	rexbii 1671	. 2
45	41, 44	sylib 198	1 $/\$ $\/$

Colors of variables: wff set class

Syntax hints:

wn 2

wi 3 $\/$ wo 222 $/\$ wa 223 $\/$ w3o 776 $/\$ w3a 777

wal 956

wceq 958

wcel 960

wral 1648

wrex 1649

cvv 1814

wss 2050

wpss 2051

cuni 2507 class class class wbr 2624

copab 2671

wpo 2844

wor 2845

This theorem is referenced by: infxpidmlem9 7561

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 964 ax-gen 965 ax-8 966 ax-9 967 ax-10 968 ax-11 969 ax-12 970 ax-13 971 ax-14 972 ax-17 973 ax-4 975 ax-5o 977 ax-6o 980 ax-9o 1125 ax-10o 1142 ax-16 1212 ax-11o 1220 ax-ext 1462 ax-rep 2698 ax-sep 2708 ax-nul 2715 ax-pow 2748 ax-pr 2785 ax-un 2872 ax-ac 4754

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 778 df-3an 779 df-ex 983 df-sb 1174 df-eu 1384 df-mo 1385 df-clab 1467 df-cleq 1472 df-clel 1475 df-ne 1590 df-ral 1652 df-rex 1653 df-reu 1654 df-rab 1655 df-v 1815 df-sbc 1945 df-dif 2052 df-un 2053 df-in 2054 df-ss 2056 df-pss 2058 df-nul 2284 df-pw 2406 df-sn 2416 df-pr 2417 df-tp 2419 df-op 2420 df-uni 2508 df-int 2538 df-iun 2572 df-br 2625 df-opab 2672 df-tr 2686 df-eprel 2838 df-id 2841 df-po 2846 df-so 2856 df-fr 2923 df-we 2940 df-ord 2957 df-on 2958 df-suc 2960 df-xp 3190 df-rel 3191 df-cnv 3192 df-co 3193 df-dm 3194 df-rn 3195 df-res 3196 df-ima 3197 df-fun 3198 df-fn 3199 df-f 3200 df-f1 3201 df-fo 3202 df-f1o 3203 df-fv 3204 df-iso 3205