Theorem zorn 3611

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 zornlem1 3603 through zornlem7 3609; this final piece mainly changes bound variables to eliminate the hypotheses of zornlem7 3609.

Hypothesis

Ref	Expression
zorn.1	|- A e. V

Assertion

Ref	Expression
zorn	|- ((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 group(s):   x,y,z,w,R   x,A,y,z,w

Proof of Theorem zorn

Step	Hyp	Ref	Expression
1		zorn.1	. 2 |- A e. V
2		rdglem1 2975	. 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 hqRv} | A.k e. {v e. A | A.q e. ran hqRv} -. 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 hqRv} | A.k e. {v e. A | A.q e. ran hqRv} -. kqm}}` (d |` g)))}
3		cleqid 1102	. 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 hqRv} | A.k e. {v e. A | A.q e. ran hqRv} -. 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 hqRv} | A.k e. {v e. A | A.q e. ran hqRv} -. kqm}}` (a |` c)))}
4		breq2 2066	. . . . 5 |- (v = r -> (sRv <-> sRr))
5	4	biraldv 1219	. . . 4 |- (v = r -> (A.s e. ran dsRv <-> A.s e. ran dsRr))
6		breq1 2065	. . . . 5 |- (q = s -> (qRv <-> sRv))
7	6	cbvralv 1333	. . . 4 |- (A.q e. ran dqRv <-> A.s e. ran dsRv)
8	5, 7	syl5bb 410	. . 3 |- (v = r -> (A.q e. ran dqRv <-> A.s e. ran dsRr))
9	8	cbvrabv 1426	. 2 |- {v e. A | A.q e. ran dqRv} = {r e. A | A.s e. ran dsRr}
10		cleqid 1102	. 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 hqRv} | A.k e. {v e. A | A.q e. ran hqRv} -. 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 hqRv} | A.k e. {v e. A | A.q e. ran hqRv} -. kqm}}` (a |` c)))}"t)sRr}
11		id 9	. . . 4 |- (k = g -> k = g)
12		rneq 2555	. . . . . . . . . . . 12 |- (h = d -> ran h = ran d)
13		raleq 1324	. . . . . . . . . . . 12 |- (ran h = ran d -> (A.q e. ran hqRv <-> A.q e. ran dqRv))
14	12, 13	syl 12	. . . . . . . . . . 11 |- (h = d -> (A.q e. ran hqRv <-> A.q e. ran dqRv))
15	14	birabsdv 1344	. . . . . . . . . 10 |- (h = d -> {v e. A | A.q e. ran hqRv} = {v e. A | A.q e. ran dqRv})
16	15	eleq2d 1156	. . . . . . . . 9 |- (h = d -> (n e. {v e. A | A.q e. ran hqRv} <-> n e. {v e. A | A.q e. ran dqRv}))
17		raleq 1324	. . . . . . . . . . 11 |- ({v e. A | A.q e. ran hqRv} = {v e. A | A.q e. ran dqRv} -> (A.j e. {v e. A | A.q e. ran hqRv} -. jqn <-> A.j e. {v e. A | A.q e. ran dqRv} -. jqn))
18		breq1 2065	. . . . . . . . . . . . 13 |- (k = j -> (kqn <-> jqn))
19	18	negbid 463	. . . . . . . . . . . 12 |- (k = j -> (-. kqn <-> -. jqn))
20	19	cbvralv 1333	. . . . . . . . . . 11 |- (A.k e. {v e. A | A.q e. ran hqRv} -. kqn <-> A.j e. {v e. A | A.q e. ran hqRv} -. jqn)
21	17, 20	syl5bb 410	. . . . . . . . . 10 |- ({v e. A | A.q e. ran hqRv} = {v e. A | A.q e. ran dqRv} -> (A.k e. {v e. A | A.q e. ran hqRv} -. kqn <-> A.j e. {v e. A | A.q e. ran dqRv} -. jqn))
22	15, 21	syl 12	. . . . . . . . 9 |- (h = d -> (A.k e. {v e. A | A.q e. ran hqRv} -. kqn <-> A.j e. {v e. A | A.q e. ran dqRv} -. jqn))
23	16, 22	anbi12d 476	. . . . . . . 8 |- (h = d -> ((n e. {v e. A | A.q e. ran hqRv} /\ A.k e. {v e. A | A.q e. ran hqRv} -. kqn) <-> (n e. {v e. A | A.q e. ran dqRv} /\ A.j e. {v e. A | A.q e. ran dqRv} -. jqn)))
24	23	biabdv 1183	. . . . . . 7 |- (h = d -> {n | (n e. {v e. A | A.q e. ran hqRv} /\ A.k e. {v e. A | A.q e. ran hqRv} -. kqn)} = {n | (n e. {v e. A | A.q e. ran dqRv} /\ A.j e. {v e. A | A.q e. ran dqRv} -. jqn)})
25		eleq1 1149	. . . . . . . . 9 |- (m = n -> (m e. {v e. A | A.q e. ran hqRv} <-> n e. {v e. A | A.q e. ran hqRv}))
26		breq2 2066	. . . . . . . . . . 11 |- (m = n -> (kqm <-> kqn))
27	26	negbid 463	. . . . . . . . . 10 |- (m = n -> (-. kqm <-> -. kqn))
28	27	biraldv 1219	. . . . . . . . 9 |- (m = n -> (A.k e. {v e. A | A.q e. ran hqRv} -. kqm <-> A.k e. {v e. A | A.q e. ran hqRv} -. kqn))
29	25, 28	anbi12d 476	. . . . . . . 8 |- (m = n -> ((m e. {v e. A | A.q e. ran hqRv} /\ A.k e. {v e. A | A.q e. ran hqRv} -. kqm) <-> (n e. {v e. A | A.q e. ran hqRv} /\ A.k e. {v e. A | A.q e. ran hqRv} -. kqn)))
30	29	cbvabv 1424	. . . . . . 7 |- {m | (m e. {v e. A | A.q e. ran hqRv} /\ A.k e. {v e. A | A.q e. ran hqRv} -. kqm)} = {n | (n e. {v e. A | A.q e. ran hqRv} /\ A.k e. {v e. A | A.q e. ran hqRv} -. kqn)}
31	24, 30	syl5eq 1136	. . . . . 6 |- (h = d -> {m | (m e. {v e. A | A.q e. ran hqRv} /\ A.k e. {v e. A | A.q e. ran hqRv} -. kqm)} = {n | (n e. {v e. A | A.q e. ran dqRv} /\ A.j e. {v e. A | A.q e. ran dqRv} -. jqn)})
32		df-rab 1208	. . . . . 6 |- {m e. {v e. A | A.q e. ran hqRv} | A.k e. {v e. A | A.q e. ran hqRv} -. kqm} = {m | (m e. {v e. A | A.q e. ran hqRv} /\ A.k e. {v e. A | A.q e. ran hqRv} -. kqm)}
33		df-rab 1208	. . . . . 6 |- {n e. {v e. A | A.q e. ran dqRv} | A.j e. {v e. A | A.q e. ran dqRv} -. jqn} = {n | (n e. {v e. A | A.q e. ran dqRv} /\ A.j e. {v e. A | A.q e. ran dqRv} -. jqn)}
34	31, 32, 33	3eqtr4g 1147	. . . . 5 |- (h = d -> {m e. {v e. A | A.q e. ran hqRv} | A.k e. {v e. A | A.q e. ran hqRv} -. kqm} = {n e. {v e. A | A.q e. ran dqRv} | A.j e. {v e. A | A.q e. ran dqRv} -. jqn})
35	34	unieqd 1929	. . . 4 |- (h = d -> U.{m e. {v e. A | A.q e. ran hqRv} | A.k e. {v e. A | A.q e. ran hqRv} -. kqm} = U.{n e. {v e. A | A.q e. ran dqRv} | A.j e. {v e. A | A.q e. ran dqRv} -. jqn})
36	11, 35	cleqan12rd 1117	. . 3 |- ((h = d