Theorem zornlem6 3608

Description: Lemma for Zorn's lemma.

Hypotheses

Ref	Expression
zornlem.1	|- A e. V
zornlem.2	|- B = {f | E.h e. On (f Fn h /\ A.t e. h (f` t) = (G` (f |` t)))}
zornlem.3	|- F = U.B
zornlem.4	|- C = {z e. A | A.g e. ran fgRz}
zornlem.5	|- D = {z e. A | A.g e. (F"x)gRz}
zornlem.6	|- G = {<.f, t>. | t = U.{v e. C | A.u e. C -. uwv}}
zornlem.7	|- H = {z e. A | A.g e. (F"y)gRz}

Assertion

Ref	Expression
zornlem6	|- (R Po A -> (((w We A /\ x e. On) /\ A.y e. x -. H = (/)) -> R Or (F"x)))

Distinct variable group(s):   x,y,w,h,t,z,f,g,u,v,A   B,h,t,f   x,F,y,z,v,u,f,g,h,t   h,G,t,f   t,C   y,D,u,v,f,t   x,R,y,z,w,g,u,v,f,t   x,H,u,v,f,t

Proof of Theorem zornlem6

Step	Hyp	Ref	Expression
1		zornlem.1	. . . . . 6 |- A e. V
2		zornlem.2	. . . . . 6 |- B = {f | E.h e. On (f Fn h /\ A.t e. h (f` t) = (G` (f |` t)))}
3		zornlem.3	. . . . . 6 |- F = U.B
4		zornlem.4	. . . . . 6 |- C = {z e. A | A.g e. ran fgRz}
5		zornlem.5	. . . . . 6 |- D = {z e. A | A.g e. (F"x)gRz}
6		zornlem.6	. . . . . 6 |- G = {<.f, t>. | t = U.{v e. C | A.u e. C -. uwv}}
7		zornlem.7	. . . . . 6 |- H = {z e. A | A.g e. (F"y)gRz}
8	1, 2, 3, 4, 5, 6, 7	zornlem5 3607	. . . . 5 |- (((w We A /\ x e. On) /\ A.y e. x -. H = (/)) -> (F"x) (_ A)
9		poss 2129	. . . . 5 |- ((F"x) (_ A -> (R Po A -> R Po (F"x)))
10	8, 9	syl 12	. . . 4 |- (((w We A /\ x e. On) /\ A.y e. x -. H = (/)) -> (R Po A -> R Po (F"x)))
11	10	com12 13	. . 3 |- (R Po A -> (((w We A /\ x e. On) /\ A.y e. x -. H = (/)) -> R Po (F"x)))
12		onelon 2223	. . . . . . . . . . . . . . . . . 18 |- ((x e. On /\ a e. x) -> a e. On)
13		onelon 2223	. . . . . . . . . . . . . . . . . 18 |- ((x e. On /\ b e. x) -> b e. On)
14	12, 13	anim12i 268	. . . . . . . . . . . . . . . . 17 |- (((x e. On /\ a e. x) /\ (x e. On /\ b e. x)) -> (a e. On /\ b e. On))
15	14	anandis 394	. . . . . . . . . . . . . . . 16 |- ((x e. On /\ (a e. x /\ b e. x)) -> (a e. On /\ b e. On))
16	15	exp 291	. . . . . . . . . . . . . . 15 |- (x e. On -> ((a e. x /\ b e. x) -> (a e. On /\ b e. On)))
17		cleqid 1102	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- {z e. A | A.g e. (F"b)gRz} = {z e. A | A.g e. (F"b)gRz}
18	1, 2, 3, 4, 17, 6	zornlem2 3604	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((b e. On /\ (w We A /\ -. {z e. A | A.g e. (F"b)gRz} = (/))) -> (a e. b -> (F` a)R(F` b)))
19	18	adantll 309	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((a e. On /\ b e. On) /\ (w We A /\ -. {z e. A | A.g e. (F"b)gRz} = (/))) -> (a e. b -> (F` a)R(F` b)))
20		breq12 2067	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((F` a) = r /\ (F` b) = s) -> ((F` a)R(F` b) <-> rRs))
21	20	biimpcd 137	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F` a)R(F` b) -> (((F` a) = r /\ (F` b) = s) -> rRs))
22	19, 21	syl6 23	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((a e. On /\ b e. On) /\ (w We A /\ -. {z e. A | A.g e. (F"b)gRz} = (/))) -> (a e. b -> (((F` a) = r /\ (F` b) = s) -> rRs)))
23	22	com23 32	. . . . . . . . . . . . . . . . . . . . . 22 |- (((a e. On /\ b e. On) /\ (w We A /\ -. {z e. A | A.g e. (F"b)gRz} = (/))) -> (((F` a) = r /\ (F` b) = s) -> (a e. b -> rRs)))
24	23	adantrrl 318	. . . . . . . . . . . . . . . . . . . . 21 |- (((a e. On /\ b e. On) /\ (w We A /\ (-. {z e. A | A.g e. (F"a)gRz} = (/) /\ -. {z e. A | A.g e. (F"b)gRz} = (/)))) -> (((F` a) = r /\ (F` b) = s) -> (a e. b -> rRs)))
25	24	imp 277	. . . . . . . . . . . . . . . . . . . 20 |- ((((a e. On /\ b e. On) /\ (w We A /\ (-. {z e. A | A.g e. (F"a)gRz} = (/) /\ -. {z e. A | A.g e. (F"b)gRz} = (/)))) /\ ((F` a) = r /\ (F` b) = s)) -> (a e. b -> rRs))
26		cleq12 1113	. . . . . . . . . . . . . . . . . . . . . 22 |- (((F` a) = r /\ (F` b) = s) -> ((F` a) = (F` b) <-> r = s))
27		fveq2 2832	. . . . . . . . . . . . . . . . . . . . . 22 |- (a = b -> (F` a) = (F` b))
28	26, 27	syl5bi 183	. . . . . . . . . . . . . . . . . . . . 21 |- (((F` a) = r /\ (F` b) = s) -> (a = b -> r = s))
29	28	adantl 305	. . . . . . . . . . . . . . . . . . . 20 |- ((((a e. On /\ b e. On) /\ (w We A /\ (-. {z e. A | A.g e. (F"a)gRz} = (/) /\ -. {z e. A | A.g e. (F"b)gRz} = (/)))) /\ ((F` a) = r /\ (F` b) = s)) -> (a = b -> r = s))
30		cleqid 1102	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- {z e. A | A.g e. (F"a)gRz} = {z e. A | A.g e. (F"a)gRz}
31	1, 2, 3, 4, 30, 6	zornlem2 3604	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((a e. On /\ (w We A /\ -. {z e. A | A.g e. (F"a)gRz} = (/))) -> (b e. a -> (F` b)R(F` a)))
32	31	adantlr 310	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((a e. On /\ b e. On) /\ (w We A /\ -. {z e. A | A.g e. (F"a)gRz} = (/))) -> (b e. a -> (F` b)R(F` a)))
33		breq12 2067	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((F` b) = s /\ (F` a) = r) -> ((F` b)R(F` a) <-> sRr))
34	33	ancoms 334	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((F` a) = r /\ (F` b) = s) -> ((F` b)R(F` a) <-> sRr))
35	34	biimpcd 137	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F` b)R(F` a) -> (((F` a) = r /\ (F` b) = s) -> sRr))
36	32, 35	syl6 23	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((a e. On /\ b e. On) /\ (w We A /\ -. {z e. A | A.g e. (F"a)gRz} = (/))) -> (b e. a -> (((F` a) = r /\ (F` b) = s) -> sRr)))
37	36	com23 32	. . . . . . . . . . . . . . . . . . . . . 22 |- (((a e. On /\ b e. On) /\ (w We A /\ -. {z e. A | A.g e. (F"a)gRz} = (/))) -> (((F` a) = r /\ (F` b) = s) -> (b e. a -> sRr)))
38	37	adantrrr 319	. . . . . . . . . . . . . . . . . . . . 21 |- (((a e. On /\ b e. On) /\ (w We A /\ (-. {z e. A | A.g e. (F"a)gRz} = (/) /\ -. {z e. A | A.g e. (F"b)gRz} = (/)))) -> (((F` a) = r /\ (F` b) = s) -> (b e. a -> sRr)))
39	38	imp 277	. . . . . . . . . . . . . . . . . . . 20 |- ((((a e. On /\ b e. On) /\ (w We A /\ (-. {z e. A | A.g e. (F"a)gRz} = (/) /\ -. {z e. A | A.g e. (F"b)gRz} = (/)))) /\ ((F` a) = r /\ (F` b) = s)) -> (b e. a -> sRr))
40	25, 29, 39	im3ord 637	. . . . . . . . . . . . . . . . . . 19 |- ((((a e. On /\ b e. On) /\ (w We A /\ (-. {z e. A | A.g e. (F"a)gRz} = (/) /\ -. {z e. A | A.g e. (F"b)gRz} = (/)))) /\ ((F` a) = r /\ (F` b) = s)) -> ((a e. b \/ a = b \/ b e. a) -> (rRs \/ r = s \/ sRr)))
41		ordtri3or 2230	. . . . . . . . . . . . . . . . . . . 20 |- ((Ord a /\ Ord b) -> (a e. b \/ a = b \/ b e. a))
42		eloni 2209	. . . . . . . . . . . . . . . . . . . 20 |- (a e. On -> Ord a)
43		eloni 2209	. . . . . . . . . . . . . . . . . . . 20 |- (b e. On -> Ord b)
44	41, 42, 43	syl2an 349	. . . . . . . . . . . . . . . . . . 19 |- ((a e. On /\ b e. On) -> (a e. b \/ a = b \/ b e. a))
45	40, 44	syl5 22	. . . . . . . . . . . . . . . . . 18 |- ((((