Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem zorn2 4768

Description: Zorn's Lemma of [Monk1] p. 117. This theorem is equivalent to the Axiom of Choice and states that every partially ordered set (with an ordering relation ) in which every totally ordered subset has an upper bound, contains at least one maximal element. The main proof consists of lemmas zorn2lem1 4760 through zorn2lem7 4766; this final piece mainly changes bound variables to eliminate the hypotheses of zorn2lem7 4766.

Hypothesis

Ref	Expression
zorn2.1

Assertion

Ref	Expression
zorn2

Distinct variable groups:   ,,,,   ,,,,

---

Proof of Theorem zorn2

Step	Hyp	Ref	Expression
1		zorn2.1	. 2
2		rdglem1 3922	. 2
3		eqid 1468	. 2
4		breq2 2613	. . . . 5
5	4	ralbidv 1655	. . . 4
6		breq1 2612	. . . . 5
7	6	cbvralv 1791	. . . 4
8	5, 7	syl5bb 530	. . 3
9	8	cbvrabv 1902	. 2
10		eqid 1468	. 2
11		id 59	. . . 4
12		rneq 3328	. . . . . . . . . . . 12
13	12	raleq1d 1781	. . . . . . . . . . 11
14	13	rabbisdv 1798	. . . . . . . . . 10
15	14	eleq2d 1533	. . . . . . . . 9
16		raleq1 1778	. . . . . . . . . . 11
17		breq1 2612	. . . . . . . . . . . . 13
18	17	negbid 609	. . . . . . . . . . . 12
19	18	cbvralv 1791	. . . . . . . . . . 11
20	16, 19	syl5bb 530	. . . . . . . . . 10
21	14, 20	syl 10	. . . . . . . . 9
22	15, 21	anbi12d 626	. . . . . . . 8
23	22	abbidv 1569	. . . . . . 7
24		eleq1 1526	. . . . . . . . 9
25		breq2 2613	. . . . . . . . . . 11
26	25	negbid 609	. . . . . . . . . 10
27	26	ralbidv 1655	. . . . . . . . 9
28	24, 27	anbi12d 626	. . . . . . . 8
29	28	cbvabv 1900	. . . . . . 7
30	23, 29	syl5eq 1511	. . . . . 6
31		df-rab 1644	. . . . . 6
32		df-rab 1644	. . . . . 6
33	30, 31, 32	3eqtr4g 1523	. . . . 5
34	33	unieqd 2502	. . . 4