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 A (with an ordering relation R) 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	|- A e. V

Assertion

Ref	Expression
zorn2	|- ((R Po A /\ A.w((w (_ A /\ R Or w) -> E.x e. A A.z e. w (zRx \/ z = x))) -> E.x e. A A.y e. A -. xRy)

Distinct variable groups:   x,y,z,w,R   x,A,y,z,w

Proof of Theorem zorn2

Step	Hyp	Ref	Expression
1		zorn2.1	. 2 |- A e. V
2		rdglem1 3922	. 2 |- {a | E.b e. On (a Fn b /\ A.c e. b (a` c) = ({<.h, k>. | k = U.{m e. {v e. A | A.q e. ran h qRv} | A.k e. {v e. A | A.q e. ran h qRv} -. kqm}}` (a |` c)))} = {d | E.f e. On (d Fn f /\ A.g e. f (d` g) = ({<.h, k>. | k = U.{m e. {v e. A | A.q e. ran h qRv} | A.k e. {v e. A | A.q e. ran h qRv} -. kqm}}` (d |` g)))}
3		eqid 1468	. 2 |- U.{a | E.b e. On (a Fn b /\ A.c e. b (a` c) = ({<.h, k>. | k = U.{m e. {v e. A | A.q e. ran h qRv} | A.k e. {v e. A | A.q e. ran h qRv} -. kqm}}` (a |` c)))} = U.{a | E.b e. On (a Fn b /\ A.c e. b (a` c) = ({<.h, k>. | k = U.{m e. {v e. A | A.q e. ran h qRv} | A.k e. {v e. A | A.q e. ran h qRv} -. kqm}}` (a |` c)))}
4		breq2 2613	. . . . 5 |- (v = r -> (sRv <-> sRr))
5	4	ralbidv 1655	. . . 4 |- (v = r -> (A.s e. ran d sRv <-> A.s e. ran d sRr))
6		breq1 2612	. . . . 5 |- (q = s -> (qRv <-> sRv))
7	6	cbvralv 1791	. . . 4 |- (A.q e. ran d qRv <-> A.s e. ran d sRv)
8	5, 7	syl5bb 530	. . 3 |- (v = r -> (A.q e. ran d qRv <-> A.s e. ran d sRr))
9	8	cbvrabv 1902	. 2 |- {v e. A | A.q e. ran d qRv} = {r e. A | A.s e. ran d sRr}
10		eqid 1468	. 2 |- {r e. A | A.s e. (U.{a | E.b e. On (a Fn b /\ A.c e. b (a` c) = ({<.h, k>. | k = U.{m e. {v e. A | A.q e. ran h qRv} | A.k e. {v e. A | A.q e. ran h qRv} -. kqm}}` (a |` c)))}"t)sRr} = {r e. A | A.s e. (U.{a | E.b e. On (a Fn b /\ A.c e. b (a` c) = ({<.h, k>. | k = U.{m e. {v e. A | A.q e. ran h qRv} | A.k e. {v e. A | A.q e. ran h qRv} -. kqm}}` (a |` c)))}"t)sRr}
11		id 59	. . . 4 |- (k = g -> k = g)
12		rneq 3328	. . . . . . . . . . . 12 |- (h = d -> ran h = ran d)
13	12	raleq1d 1781	. . . . . . . . . . 11 |- (h = d -> (A.q e. ran h qRv <-> A.q e. ran d qRv))
14	13	rabbisdv 1798	. . . . . . . . . 10 |- (h = d -> {v e. A | A.q e. ran h qRv} = {v e. A | A.q e. ran d qRv})
15	14	eleq2d 1533	. . . . . . . . 9 |- (h = d -> (n e. {v e. A | A.q e. ran h qRv} <-> n e. {v e. A | A.q e. ran d qRv}))
16		raleq1 1778	. . . . . . . . . . 11 |- ({v e. A | A.q e. ran h qRv} = {v e. A | A.q e. ran d qRv} -> (A.j e. {v e. A | A.q e. ran h qRv} -. jqn <-> A.j e. {v e. A | A.q e. ran d qRv} -. jqn))
17		breq1 2612	. . . . . . . . . . . . 13 |- (k = j -> (kqn <-> jqn))
18	17	negbid 609	. . . . . . . . . . . 12 |- (k = j -> (-. kqn <-> -. jqn))
19	18	cbvralv 1791	. . . . . . . . . . 11 |- (A.k e. {v e. A | A.q e. ran h qRv} -. kqn <-> A.j e. {v e. A | A.q e. ran h qRv} -. jqn)
20	16, 19	syl5bb 530	. . . . . . . . . 10 |- ({v e. A | A.q e. ran h qRv} = {v e. A | A.q e. ran d qRv} -> (A.k e. {v e. A | A.q e. ran h qRv} -. kqn <-> A.j e. {v e. A | A.q e. ran d qRv} -. jqn))
21	14, 20	syl 10	. . . . . . . . 9 |- (h = d -> (A.k e. {v e. A | A.q e. ran h qRv} -. kqn <-> A.j e. {v e. A | A.q e. ran d qRv} -. jqn))
22	15, 21	anbi12d 626	. . . . . . . 8 |- (h = d -> ((n e. {v e. A | A.q e. ran h qRv} /\ A.k e. {v e. A | A.q e. ran h qRv} -. kqn) <-> (n e. {v e. A | A.q e. ran d qRv} /\ A.j e. {v e. A | A.q e. ran d qRv} -. jqn)))
23	22	abbidv 1569	. . . . . . 7 |- (h = d -> {n | (n e. {v e. A | A.q e. ran h qRv} /\ A.k e. {v e. A | A.q e. ran h qRv} -. kqn)} = {n | (n e. {v e. A | A.q e. ran d qRv} /\ A.j e. {v e. A | A.q e. ran d qRv} -. jqn)})
24		eleq1 1526	. . . . . . . . 9 |- (m = n -> (m e. {v e. A | A.q e. ran h qRv} <-> n e. {v e. A | A.q e. ran h qRv}))
25		breq2 2613	. . . . . . . . . . 11 |- (m = n -> (kqm <-> kqn))
26	25	negbid 609	. . . . . . . . . 10 |- (m = n -> (-. kqm <-> -. kqn))
27	26	ralbidv 1655	. . . . . . . . 9 |- (m = n -> (A.k e. {v e. A | A.q e. ran h qRv} -. kqm <-> A.k e. {v e. A | A.q e. ran h qRv} -. kqn))
28	24, 27	anbi12d 626	. . . . . . . 8 |- (m = n -> ((m e. {v e. A | A.q e. ran h qRv} /\ A.k e. {v e. A | A.q e. ran h qRv} -. kqm) <-> (n e. {v e. A | A.q e. ran h qRv} /\ A.k e. {v e. A | A.q e. ran h qRv} -. kqn)))
29	28	cbvabv 1900	. . . . . . 7 |- {m | (m e. {v e. A | A.q e. ran h qRv} /\ A.k e. {v e. A | A.q e. ran h qRv} -. kqm)} = {n | (n e. {v e. A | A.q e. ran h qRv} /\ A.k e. {v e. A | A.q e. ran h qRv} -. kqn)}
30	23, 29	syl5eq 1511	. . . . . 6 |- (h = d -> {m | (m e. {v e. A | A.q e. ran h qRv} /\ A.k e. {v e. A | A.q e. ran h qRv} -. kqm)} = {n | (n e. {v e. A | A.q e. ran d qRv} /\ A.j e. {v e. A | A.q e. ran d qRv} -. jqn)})
31		df-rab 1644	. . . . . 6 |- {m e. {v e. A | A.q e. ran h qRv} | A.k e. {v e. A | A.q e. ran h qRv} -. kqm} = {m | (m e. {v e. A | A.q e. ran h qRv} /\ A.k e. {v e. A | A.q e. ran h qRv} -. kqm)}
32		df-rab 1644	. . . . . 6 |- {n e. {v e. A | A.q e. ran d qRv} | A.j e. {v e. A | A.q e. ran d qRv} -. jqn} = {n | (n e. {v e. A | A.q e. ran d qRv} /\ A.j e. {v e. A | A.q e. ran d qRv} -. jqn)}
33	30, 31, 32	3eqtr4g 1523	. . . . 5 |- (h = d -> {m e. {v e. A | A.q e. ran h qRv} | A.k e. {v e. A | A.q e. ran h qRv} -. kqm} = {n e. {v e. A | A.q e. ran d qRv} | A.j e. {v e. A | A.q e. ran d qRv} -. jqn})
34	33	unieqd 2502	. . . 4 |- (h = d -> U.{m e. {v e. A | A.q e. ran h qRv} | A.k e. {v e. A | A.q e. ran h qRv} -. kqm} = U.{n e. {v e. A | A.q e. ran d qRv} | A.j e. {v e. A | A.q e. ran d qRv} -. jqn