Theorem zorn2 4776

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 4768 through zorn2lem7 4774; this final piece mainly changes bound variables to eliminate the hypotheses of zorn2lem7 4774.

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 3928	. 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 1473	. 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 2618	. . . . 5 |- (v = r -> (sRv <-> sRr))
5	4	ralbidv 1660	. . . 4 |- (v = r -> (A.s e. ran d sRv <-> A.s e. ran d sRr))
6		breq1 2617	. . . . 5 |- (q = s -> (qRv <-> sRv))
7	6	cbvralv 1796	. . . 4 |- (A.q e. ran d qRv <-> A.s e. ran d sRv)
8	5, 7	syl5bb 531	. . 3 |- (v = r -> (A.q e. ran d qRv <-> A.s e. ran d sRr))
9	8	cbvrabv 1907	. 2 |- {v e. A | A.q e. ran d qRv} = {r e. A | A.s e. ran d sRr}
10		eqid 1473	. 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 3334	. . . . . . . . . . . 12 |- (h = d -> ran h = ran d)
13	12	raleq1d 1786	. . . . . . . . . . 11 |- (h = d -> (A.q e. ran h qRv <-> A.q e. ran d qRv))
14	13	rabbisdv 1803	. . . . . . . . . 10 |- (h = d -> {v e. A | A.q e. ran h qRv} = {v e. A | A.q e. ran d qRv})
15	14	eleq2d 1538	. . . . . . . . 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 1783	. . . . . . . . . . 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 2617	. . . . . . . . . . . . 13 |- (k = j -> (kqn <-> jqn))
18	17	negbid 610	. . . . . . . . . . . 12 |- (k = j -> (-. kqn <-> -. jqn))
19	18	cbvralv 1796	. . . . . . . . . . 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 531	. . . . . . . . . 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 627	. . . . . . . 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 1574	. . . . . . 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 1531	. . . . . . . . 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 2618	. . . . . . . . . . 11 |- (m = n -> (kqm <-> kqn))
26	25	negbid 610	. . . . . . . . . 10 |- (m = n -> (-. kqm <-> -. kqn))
27	26	ralbidv 1660	. . . . . . . . 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 627	. . . . . . . 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 1905	. . . . . . 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 1516	. . . . . 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 1649	. . . . . 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 1649	. . . . . 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 1528	. . . . 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 2507	. . . 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