Theorem zorn2lem6 4773

Description: Lemma for zorn2 4776.

Hypotheses

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

Assertion

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

Distinct variable groups:   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 zorn2lem6

Step	Hyp	Ref	Expression
1		zorn2lem.1	. . . . . 6 |- A e. V
2		zorn2lem.2	. . . . . 6 |- B = {f | E.h e. On (f Fn h /\ A.t e. h (f` t) = (G` (f |` t)))}
3		zorn2lem.3	. . . . . 6 |- F = U.B
4		zorn2lem.4	. . . . . 6 |- C = {z e. A | A.g e. ran f gRz}
5		zorn2lem.5	. . . . . 6 |- D = {z e. A | A.g e. (F"x)gRz}
6		zorn2lem.6	. . . . . 6 |- G = {<.f, t>. | t = U.{v e. C | A.u e. C -. uwv}}
7		zorn2lem.7	. . . . . 6 |- H = {z e. A | A.g e. (F"y)gRz}
8	1, 2, 3, 4, 5, 6, 7	zorn2lem5 4772	. . . . 5 |- (((w We A /\ x e. On) /\ A.y e. x H =/= (/)) -> (F"x) (_ A)
9		poss 2836	. . . . 5 |- ((F"x) (_ A -> (R Po A -> R Po (F"x)))
10	8, 9	syl 10	. . . 4 |- (((w We A /\ x e. On) /\ A.y e. x H =/= (/)) -> (R Po A -> R Po (F"x)))
11	10	com12 11	. . 3 |- (R Po A -> (((w We A /\ x e. On) /\ A.y e. x H =/= (/)) -> R Po (F"x)))
12		onelon 2967	. . . . . . . . . . . . . . . . . 18 |- ((x e. On /\ b e. x) -> b e. On)
13		onelon 2967	. . . . . . . . . . . . . . . . . 18 |- ((x e. On /\ a e. x) -> a e. On)
14	12, 13	anim12i 333	. . . . . . . . . . . . . . . . 17 |- (((x e. On /\ b e. x) /\ (x e. On /\ a e. x)) -> (b e. On /\ a e. On))
15	14	anandis 512	. . . . . . . . . . . . . . . 16 |- ((x e. On /\ (b e. x /\ a e. x)) -> (b e. On /\ a e. On))
16	15	ex 373	. . . . . . . . . . . . . . 15 |- (x e. On -> ((b e. x /\ a e. x) -> (b e. On /\ a e. On)))
17		eqid 1473	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- {z e. A | A.g e. (F"a)gRz} = {z e. A | A.g e. (F"a)gRz}
18	1, 2, 3, 4, 17, 6	zorn2lem2 4769	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((a e. On /\ (w We A /\ {z e. A | A.g e. (F"a)gRz} =/= (/))) -> (b e. a -> (F` b)R(F` a)))
19	18	adantll 392	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((b e. On /\ a e. On) /\ (w We A /\ {z e. A | A.g e. (F"a)gRz} =/= (/))) -> (b e. a -> (F` b)R(F` a)))
20		breq12 2619	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((F` b) = s /\ (F` a) = r) -> ((F` b)R(F` a) <-> sRr))
21	20	biimpcd 155	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F` b)R(F` a) -> (((F` b) = s /\ (F` a) = r) -> sRr))
22	19, 21	syl6 22	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((b e. On /\ a e. On) /\ (w We A /\ {z e. A | A.g e. (F"a)gRz} =/= (/))) -> (b e. a -> (((F` b) = s /\ (F` a) = r) -> sRr)))
23	22	com23 32	. . . . . . . . . . . . . . . . . . . . . 22 |- (((b e. On /\ a e. On) /\ (w We A /\ {z e. A | A.g e. (F"a)gRz} =/= (/))) -> (((F` b) = s /\ (F` a) = r) -> (b e. a -> sRr)))
24	23	adantrrl 402	. . . . . . . . . . . . . . . . . . . . 21 |- (((b e. On /\ a e. On) /\ (w We A /\ ({z e. A | A.g e. (F"b)gRz} =/= (/) /\ {z e. A | A.g e. (F"a)gRz} =/= (/)))) -> (((F` b) = s /\ (F` a) = r) -> (b e. a -> sRr)))
25	24	imp 350	. . . . . . . . . . . . . . . . . . . 20 |- ((((b e. On /\ a e. On) /\ (w We A /\ ({z e. A | A.g e. (F"b)gRz} =/= (/) /\ {z e. A | A.g e. (F"a)gRz} =/= (/)))) /\ ((F` b) = s /\ (F` a) = r)) -> (b e. a -> sRr))
26		eqeq12 1484	. . . . . . . . . . . . . . . . . . . . . 22 |- (((F` b) = s /\ (F` a) = r) -> ((F` b) = (F` a) <-> s = r))
27		fveq2 3715	. . . . . . . . . . . . . . . . . . . . . 22 |- (b = a -> (F` b) = (F` a))
28	26, 27	syl5bi 208	. . . . . . . . . . . . . . . . . . . . 21 |- (((F` b) = s /\ (F` a) = r) -> (b = a -> s = r))
29	28	adantl 388	. . . . . . . . . . . . . . . . . . . 20 |- ((((b e. On /\ a e. On) /\ (w We A /\ ({z e. A | A.g e. (F"b)gRz} =/= (/) /\ {z e. A | A.g e. (F"a)gRz} =/= (/)))) /\ ((F` b) = s /\ (F` a) = r)) -> (b = a -> s = r))
30		eqid 1473	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- {z e. A | A.g e. (F"b)gRz} = {z e. A | A.g e. (F"b)gRz}
31	1, 2, 3, 4, 30, 6	zorn2lem2 4769	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((b e. On /\ (w We A /\ {z e. A | A.g e. (F"b)gRz} =/= (/))) -> (a e. b -> (F` a)R(F` b)))
32	31	adantlr 393	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((b e. On /\ a e. On) /\ (w We A /\ {z e. A | A.g e. (F"b)gRz} =/= (/))) -> (a e. b -> (F` a)R(F` b)))
33		breq12 2619	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((F` a) = r /\ (F` b) = s) -> ((F` a)R(F` b) <-> rRs))
34	33	ancoms 436	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((F` b) = s /\ (F` a) = r) -> ((F` a)R(F` b) <-> rRs))
35	34	biimpcd 155	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F` a)R(F` b) -> (((F` b) = s /\ (F` a) = r) -> rRs))
36	32, 35	syl6 22	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((b e. On /\ a e. On) /\ (w We A /\ {z e. A | A.g e. (F"b)gRz} =/= (/))) -> (a e. b -> (((F` b) = s /\ (F` a) = r) -> rRs)))
37	36	com23 32	. . . . . . . . . . . . . . . . . . . . . 22 |- (((b e. On /\ a e. On) /\ (w We A /\ {z e. A | A.g e. (F"b)gRz} =/= (/))) -> (((F` b) = s /\ (F` a) = r) -> (a e. b -> rRs)))
38	37	adantrrr 403	. . . . . . . . . . . . . . . . . . . . 21 |- (((b e. On /\ a e. On) /\ (w We A /\ ({z e. A | A.g e. (F"b)gRz} =/= (/) /\ {z e. A | A.g e. (F"a)gRz} =/= (/)))) -> (((F` b) = s /\ (F` a) = r) -> (a e. b -> rRs)))
39	38	imp 350	. . . . . . . . . . . . . . . . . . . 20 |- ((((b e. On /\ a e. On) /\ (w We A /\ ({z e. A | A.g e. (F"b)gRz} =/= (/) /\ {z e. A | A.g e. (F"a)gRz} =/= (/)))) /\ ((F` b) = s /\ (F` a) = r)) -> (a e. b -> rRs))
40	25, 29, 39	3orim123d 899	. . . . . . . . . . . . . . . . . . 19 |- ((((b e. On /\ a e. On) /\ (w We A /\ ({z e. A | A.g e. (F"b)gRz} =/= (/) /\ {z e. A | A.g e. (F"a)gRz} =/= (/)))) /\ ((F` b) = s /\ (F` a) = r)) -> ((b e. a \/ b = a \/ a e. b) -> (sRr \/ s = r \/ rRs)))
41		ordtri3or 2974	. . . . . . . . . . . . . . . . . . . 20 |- ((Ord b /\ Ord a) -> (b e. a \/ b = a \/ a e. b))
42		eloni 2953	. . . . . . . . . . . . . . . . . . . 20 |- (b e. On -> Ord b)
43		eloni 2953	. . . . . . . . . . . . . . . . . . . 20 |- (a e. On -> Ord a)
44	41, 42, 43	syl2an 454	. . . . . . . . . . . . . . . . . . 19 |- ((b e. On /\ a e. On) -> (b