Theorem spwmo 8652

Description: A poset has at most one supremum.

Hypothesis

Ref	Expression
spwmo.1	|- (ph <-> (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)))

Assertion

Ref	Expression
spwmo	|- (R e. Poset -> E*x(x e. X /\ ph))

Distinct variable groups:   x,y,z,A   x,R,y,z   x,X,y

Proof of Theorem spwmo

Step	Hyp	Ref	Expression
1		breq1 2627	. . . . . . . . . 10 |- (y = z -> (yRx <-> zRx))
2	1	cbvralv 1803	. . . . . . . . 9 |- (A.y e. A yRx <-> A.z e. A zRx)
3		breq2 2628	. . . . . . . . . . . . . . . . . 18 |- (y = w -> (zRy <-> zRw))
4	3	ralbidv 1666	. . . . . . . . . . . . . . . . 17 |- (y = w -> (A.z e. A zRy <-> A.z e. A zRw))
5		breq2 2628	. . . . . . . . . . . . . . . . 17 |- (y = w -> (xRy <-> xRw))
6	4, 5	imbi12d 628	. . . . . . . . . . . . . . . 16 |- (y = w -> ((A.z e. A zRy -> xRy) <-> (A.z e. A zRw -> xRw)))
7	6	rcla4v 1876	. . . . . . . . . . . . . . 15 |- (w e. X -> (A.y e. X (A.z e. A zRy -> xRy) -> (A.z e. A zRw -> xRw)))
8	7	imp3a 361	. . . . . . . . . . . . . 14 |- (w e. X -> ((A.y e. X (A.z e. A zRy -> xRy) /\ A.z e. A zRw) -> xRw))
9		breq2 2628	. . . . . . . . . . . . . . . . . 18 |- (y = x -> (zRy <-> zRx))
10	9	ralbidv 1666	. . . . . . . . . . . . . . . . 17 |- (y = x -> (A.z e. A zRy <-> A.z e. A zRx))
11		breq2 2628	. . . . . . . . . . . . . . . . 17 |- (y = x -> (wRy <-> wRx))
12	10, 11	imbi12d 628	. . . . . . . . . . . . . . . 16 |- (y = x -> ((A.z e. A zRy -> wRy) <-> (A.z e. A zRx -> wRx)))
13	12	rcla4v 1876	. . . . . . . . . . . . . . 15 |- (x e. X -> (A.y e. X (A.z e. A zRy -> wRy) -> (A.z e. A zRx -> wRx)))
14	13	imp3a 361	. . . . . . . . . . . . . 14 |- (x e. X -> ((A.y e. X (A.z e. A zRy -> wRy) /\ A.z e. A zRx) -> wRx))
15	8, 14	im2anan9r 566	. . . . . . . . . . . . 13 |- ((x e. X /\ w e. X) -> (((A.y e. X (A.z e. A zRy -> xRy) /\ A.z e. A zRw) /\ (A.y e. X (A.z e. A zRy -> wRy) /\ A.z e. A zRx)) -> (xRw /\ wRx)))
16		psasym 8647	. . . . . . . . . . . . . 14 |- ((R e. Poset /\ xRw /\ wRx) -> x = w)
17	16	3expib 838	. . . . . . . . . . . . 13 |- (R e. Poset -> ((xRw /\ wRx) -> x = w))
18	15, 17	syl9 57	. . . . . . . . . . . 12 |- ((x e. X /\ w e. X) -> (R e. Poset -> (((A.y e. X (A.z e. A zRy -> xRy) /\ A.z e. A zRw) /\ (A.y e. X (A.z e. A zRy -> wRy) /\ A.z e. A zRx)) -> x = w)))
19	18	com13 33	. . . . . . . . . . 11 |- (((A.y e. X (A.z e. A zRy -> xRy) /\ A.z e. A zRw) /\ (A.y e. X (A.z e. A zRy -> wRy) /\ A.z e. A zRx)) -> (R e. Poset -> ((x e. X /\ w e. X) -> x = w)))
20	19	exp43 386	. . . . . . . . . 10 |- (A.y e. X (A.z e. A zRy -> xRy) -> (A.z e. A zRw -> (A.y e. X (A.z e. A zRy -> wRy) -> (A.z e. A zRx -> (R e. Poset -> ((x e. X /\ w e. X) -> x = w))))))
21	20	com4r 41	. . . . . . . . 9 |- (A.z e. A zRx -> (A.y e. X (A.z e. A zRy -> xRy) -> (A.z e. A zRw -> (A.y e. X (A.z e. A zRy -> wRy) -> (R e. Poset -> ((x e. X /\ w e. X) -> x = w))))))
22	2, 21	sylbi 199	. . . . . . . 8 |- (A.y e. A yRx -> (A.y e. X (A.z e. A zRy -> xRy) -> (A.z e. A zRw -> (A.y e. X (A.z e. A zRy -> wRy) -> (R e. Poset -> ((x e. X /\ w e. X) -> x = w))))))
23	22	imp43 370	. . . . . . 7 |- (((A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)) /\ (A.z e. A zRw /\ A.y e. X (A.z e. A zRy -> wRy))) -> (R e. Poset -> ((x e. X /\ w e. X) -> x = w)))
24	23	com3r 35	. . . . . 6 |- ((x e. X /\ w e. X) -> (((A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)) /\ (A.z e. A zRw /\ A.y e. X (A.z e. A zRy -> wRy))) -> (R e. Poset -> x = w)))
25	24	imp 350	. . . . 5 |- (((x e. X /\ w e. X) /\ ((A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)) /\ (A.z e. A zRw /\ A.y e. X (A.z e. A zRy -> wRy)))) -> (R e. Poset -> x = w))
26	25	an4s 510	. . . 4 |- (((x e. X /\ (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))) /\ (w e. X /\ (A.z e. A zRw /\ A.y e. X (A.z e. A zRy -> wRy)))) -> (R e. Poset -> x = w))
27	26	com12 11	. . 3 |- (R e. Poset -> (((x e. X /\ (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))) /\ (w e. X /\ (A.z e. A zRw /\ A.y e. X (A.z e. A zRy -> wRy)))) -> x = w))
28	27	19.21aivv 1289	. 2 |- (R e. Poset -> A.xA.w(((x e. X /\ (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))) /\ (w e. X /\ (A.z e. A zRw /\ A.y e. X (A.z e. A zRy -> wRy)))) -> x = w))
29		spwmo.1	. . . . 5 |- (ph <-> (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)))
30	29	anbi2i 482	. . . 4 |- ((x e. X /\ ph) <-> (x e. X /\ (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))))
31	30	mobii 1407	. . 3 |- (E*x(x e. X /\ ph) <-> E*x(x e. X /\ (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))))
32		eleq1 1537	. . . . 5 |- (x = w -> (x e. X <-> w e. X))
33		breq2 2628	. . . . . . . 8 |- (x = w -> (yRx <-> yRw))
34	33	ralbidv 1666	. . . . . . 7 |- (x = w -> (A.y e. A yRx <-> A.y e. A yRw))
35		breq1 2627	. . . . . . . 8 |- (y = z -> (yRw <-> zRw))
36	35	cbvralv 1803	. . . . . . 7 |- (A.y e. A yRw <-> A.z e. A zRw)
37	34, 36	syl6bb 538	. . . . . 6 |- (x = w -> (A.y e. A yRx <-> A.z e. A zRw))
38		breq1 2627	. . . . . . . 8 |- (x = w -> (xRy <-> wRy))
39	38	imbi2d 614	. . . . . . 7 |- (x = w -> ((A.z e. A zRy -> xRy) <-> (A.z e. A zRy -> wRy)))
40	39	ralbidv 1666	. . . . . 6 |- (x = w -> (A.y e. X (A.z e. A zRy -> xRy) <-> A.y e. X (A.z e. A zRy -> wRy)))
41	37, 40	anbi12d 630	. . . . 5 |- (x = w -> ((A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)) <-> (A.z e. A zRw /\ A.y e. X (A.z e. A zRy -> wRy))))
42	32, 41	anbi12d 630	. . . 4 |- (x = w -> ((x e. X /\ (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))) <-> (w e. X /\ (A.z e. A zRw /\ A.y e. X (A.z e. A zRy -> wRy)))))
43	42	mo4 1405	. . 3 |- (E*x(x e. X /\ (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))) <-> A.xA.w(((x e. X /\ (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))) /\ (w e. X /\ (A.z e. A zRw /\ A.y e. X (A.z e. A zRy -> wRy)))) -> x = w))
44	31, 43	bitr 173	. 2 |- (E*x(x e. X /\ ph) <-> A.xA.w(((x e. X /\ (A.y e. A yRx /\