HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem zorn2lem7 4766
Description: Lemma for zorn2 4768.
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
zorn2lem7 |- ((R Po A /\ A.s((s (_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a))) -> E.a e. A A.b e. A -. aRb)
Distinct variable groups:   x,y,w,h,t,z,f,g,u,v,r,s,a,b,A   B,h,t,f   x,F,y,z,v,u,f,g,h,t,r,s,a,b   h,G,t,f   t,C   y,D,u,v,f,t,a,b   x,R,y,z,w,g,u,v,f,t,s,r,a,b   x,H,u,v,f,t,s,r,a,b
Proof of Theorem zorn2lem7
StepHypRef Expression
1 zorn2lem.1 . . 3 |- A e. V
21weth 4759 . 2 |- E.w w We A
3 zorn2lem.2 . . . . . . . 8 |- B = {f | E.h e. On (f Fn h /\ A.t e. h (f` t) = (G` (f |` t)))}
4 zorn2lem.3 . . . . . . . 8 |- F = U.B
5 zorn2lem.4 . . . . . . . 8 |- C = {z e. A | A.g e. ran f gRz}
6 zorn2lem.5 . . . . . . . 8 |- D = {z e. A | A.g e. (F"x)gRz}
7 zorn2lem.6 . . . . . . . 8 |- G = {<.f, t>. | t = U.{v e. C | A.u e. C -. uwv}}
81, 3, 4, 5, 6, 7zorn2lem4 4763 . . . . . . 7 |- ((R Po A /\ w We A) -> E.x e. On D = (/))
9 imaeq2 3386 . . . . . . . . . . . . 13 |- (x = y -> (F"x) = (F"y))
109raleq1d 1781 . . . . . . . . . . . 12 |- (x = y -> (A.g e. (F"x)gRz <-> A.g e. (F"y)gRz))
1110rabbisdv 1798 . . . . . . . . . . 11 |- (x = y -> {z e. A | A.g e. (F"x)gRz} = {z e. A | A.g e. (F"y)gRz})
12 zorn2lem.7 . . . . . . . . . . 11 |- H = {z e. A | A.g e. (F"y)gRz}
1311, 6, 123eqtr4g 1523 . . . . . . . . . 10 |- (x = y -> D = H)
1413eqeq1d 1475 . . . . . . . . 9 |- (x = y -> (D = (/) <-> H = (/)))
1514onminex 3010 . . . . . . . 8 |- (E.x e. On D = (/) -> E.x e. On (D = (/) /\ A.y e. x -. H = (/)))
16 df-ne 1579 . . . . . . . . . . 11 |- (H =/= (/) <-> -. H = (/))
1716ralbii 1659 . . . . . . . . . 10 |- (A.y e. x H =/= (/) <-> A.y e. x -. H = (/))
1817anbi2i 479 . . . . . . . . 9 |- ((D = (/) /\ A.y e. x H =/= (/)) <-> (D = (/) /\ A.y e. x -. H = (/)))
1918rexbii 1660 . . . . . . . 8 |- (E.x e. On (D = (/) /\ A.y e. x H =/= (/)) <-> E.x e. On (D = (/) /\ A.y e. x -. H = (/)))
2015, 19sylibr 200 . . . . . . 7 |- (E.x e. On D = (/) -> E.x e. On (D = (/) /\ A.y e. x H =/= (/)))
211, 3, 4, 5, 6, 7, 12zorn2lem5 4764 . . . . . . . . . . . . . . . . . . . 20 |- (((w We A /\ x e. On) /\ A.y e. x H =/= (/)) -> (F"x) (_ A)
2221a1i 8 . . . . . . . . . . . . . . . . . . 19 |- (R Po A -> (((w We A /\ x e. On) /\ A.y e. x H =/= (/)) -> (F"x) (_ A))
231, 3, 4, 5, 6, 7, 12zorn2lem6 4765 . . . . . . . . . . . . . . . . . . 19 |- (R Po A -> (((w We A /\ x e. On) /\ A.y e. x H =/= (/)) -> R Or (F"x)))
2422, 23jcad 598 . . . . . . . . . . . . . . . . . 18 |- (R Po A -> (((w We A /\ x e. On) /\ A.y e. x H =/= (/)) -> ((F"x) (_ A /\ R Or (F"x))))
253, 4tfrlem7 3902 . . . . . . . . . . . . . . . . . . . 20 |- Fun F
26 visset 1804 . . . . . . . . . . . . . . . . . . . . 21 |- x e. V
2726funimaex 3562 . . . . . . . . . . . . . . . . . . . 20 |- (Fun F -> (F"x) e. V)
2825, 27ax-mp 7 . . . . . . . . . . . . . . . . . . 19 |- (F"x) e. V
29 sseq1 2072 . . . . . . . . . . . . . . . . . . . . 21 |- (s = (F"x) -> (s (_ A <-> (F"x) (_ A))
30 soeq2 2845 . . . . . . . . . . . . . . . . . . . . 21 |- (s = (F"x) -> (R Or s <-> R Or (F"x)))
3129, 30anbi12d 626 . . . . . . . . . . . . . . . . . . . 20 |- (s = (F"x) -> ((s (_ A /\ R Or s) <-> ((F"x) (_ A /\ R Or (F"x))))
32 raleq1 1778 . . . . . . . . . . . . . . . . . . . . 21 |- (s = (F"x) -> (A.r e. s (rRa \/ r = a) <-> A.r e. (F"x)(rRa \/ r = a)))
3332rexbidv 1656 . . . . . . . . . . . . . . . . . . . 20 |- (s = (F"x) -> (E.a e. A A.r e. s (rRa \/ r = a) <-> E.a e. A A.r e. (F"x)(rRa \/ r = a)))
3431, 33imbi12d 624 . . . . . . . . . . . . . . . . . . 19 |- (s = (F"x) -> (((s (_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a)) <-> (((F"x) (_ A /\ R Or (F"x)) -> E.a e. A A.r e. (F"x)(rRa \/ r = a))))
3528, 34cla4v 1859 . . . . . . . . . . . . . . . . . 18 |- (A.s((s (_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a)) -> (((F"x) (_ A /\ R Or (F"x)) -> E.a e. A A.r e. (F"x)(rRa \/ r = a)))
3624, 35sylan9 468 . . . . . . . . . . . . . . . . 17 |- ((R Po A /\ A.s((s (_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a))) -> (((w We A /\ x e. On) /\ A.y e. x H =/= (/)) -> E.a e. A A.r e. (F"x)(rRa \/ r = a)))
3736adantld 390 . . . . . . . . . . . . . . . 16 |- ((R Po A /\ A.s((s (_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a))) -> ((D = (/) /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/))) -> E.a e. A A.r e. (F"x)(rRa \/ r = a)))
3837imp 350 . . . . . . . . . . . . . . 15 |- (((R Po A /\ A.s((s (_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a))) /\ (D = (/) /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/)))) -> E.a e. A A.r e. (F"x)(rRa \/ r = a))
39 noel 2274 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- -. b e. (/)
4021sseld 2057 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (((w We A /\ x e. On) /\ A.y e. x H =/= (/)) -> (r e. (F"x) -> r e. A))
41 potr 2837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- ((R Po A /\ (r e. A /\ a e. A /\ b e. A)) -> ((rRa /\ aRb) -> rRb))
42 3anass 777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- ((r e. A /\ a e. A /\ b e. A) <-> (r e. A /\ (a e. A /\ b e. A)))
4341, 42sylan2br 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ((R Po A /\ (r e. A /\ (a e. A /\ b e. A))) -> ((rRa /\ aRb) -> rRb))
4443exp3a 375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ((R Po A /\ (r e. A /\ (a e. A /\ b e. A))) -> (rRa -> (aRb -> rRb)))
4544com23 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ((R Po A /\ (r e. A /\ (a e. A /\ b e. A))) -> (aRb -> (rRa -> rRb)))
4645imp 350 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- (((R Po A /\ (r e. A /\ (a e. A /\ b e. A))) /\ aRb) -> (rRa -> rRb))
47 breq1 2612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- (r = a -> (rRb <-> aRb))
4847biimprcd 156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- (aRb -> (r = a -> rRb))
4948adantl 388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- (((R Po A /\ (r e. A /\ (a e. A /\ b e. A))) /\ aRb) -> (r = a -> rRb))
5046, 49jaod 424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- (((R Po A /\ (r e. A /\ (a e. A /\ b e. A))) /\ aRb) -> ((rRa \/ r = a) -> rRb))
5150exp42 383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (R Po A -> (r e. A -> ((a e. A /\ b e. A) -> (aRb -> ((rRa \/ r = a) -> rRb)))))
5240, 51sylan9r 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ((R Po A /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/))) -> (r e. (F"x) -> ((a e. A /\ b e. A) -> (aRb -> ((rRa \/ r = a) -> rRb)))))
5352com24 37 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ((R Po A /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/))) -> (aRb -> (