Theorem supmo 2156

Description: Any class B has at most one supremum in A (where R is interpreted as 'less than').

Hypothesis

Ref	Expression
supmo.1	|- R Or A

Assertion

Ref	Expression
supmo	|- E*x(x e. A /\ (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz)))

Distinct variable group(s):   x,y,z,A   x,R,y,z   x,B,y,z

Proof of Theorem supmo

Step	Hyp	Ref	Expression
1		eleq1 1149	. . . 4 |- (x = w -> (x e. A <-> w e. A))
2		breq1 2065	. . . . . . 7 |- (x = w -> (xRy <-> wRy))
3	2	negbid 463	. . . . . 6 |- (x = w -> (-. xRy <-> -. wRy))
4	3	biraldv 1219	. . . . 5 |- (x = w -> (A.y e. B -. xRy <-> A.y e. B -. wRy))
5		breq2 2066	. . . . . . 7 |- (x = w -> (yRx <-> yRw))
6	5	imbi1d 465	. . . . . 6 |- (x = w -> ((yRx -> E.z e. B yRz) <-> (yRw -> E.z e. B yRz)))
7	6	biraldv 1219	. . . . 5 |- (x = w -> (A.y e. A (yRx -> E.z e. B yRz) <-> A.y e. A (yRw -> E.z e. B yRz)))
8	4, 7	anbi12d 476	. . . 4 |- (x = w -> ((A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz)) <-> (A.y e. B -. wRy /\ A.y e. A (yRw -> E.z e. B yRz))))
9	1, 8	anbi12d 476	. . 3 |- (x = w -> ((x e. A /\ (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz))) <-> (w e. A /\ (A.y e. B -. wRy /\ A.y e. A (yRw -> E.z e. B yRz)))))
10	9	mo4 1029	. 2 |- (E*x(x e. A /\ (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz))) <-> A.xA.w(((x e. A /\ (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz))) /\ (w e. A /\ (A.y e. B -. wRy /\ A.y e. A (yRw -> E.z e. B yRz)))) -> x = w))
11		breq1 2065	. . . . . . . . . . . . . . . 16 |- (y = x -> (yRw <-> xRw))
12		breq1 2065	. . . . . . . . . . . . . . . . 17 |- (y = x -> (yRz <-> xRz))
13	12	birexdv 1220	. . . . . . . . . . . . . . . 16 |- (y = x -> (E.z e. B yRz <-> E.z e. B xRz))
14	11, 13	imbi12d 474	. . . . . . . . . . . . . . 15 |- (y = x -> ((yRw -> E.z e. B yRz) <-> (xRw -> E.z e. B xRz)))
15	14	rcla4v 1402	. . . . . . . . . . . . . 14 |- (A.y e. A (yRw -> E.z e. B yRz) -> (x e. A -> (xRw -> E.z e. B xRz)))
16	15	imp 277	. . . . . . . . . . . . 13 |- ((A.y e. A (yRw -> E.z e. B yRz) /\ x e. A) -> (xRw -> E.z e. B xRz))
17		breq2 2066	. . . . . . . . . . . . . . . . 17 |- (y = z -> (xRy <-> xRz))
18	17	negbid 463	. . . . . . . . . . . . . . . 16 |- (y = z -> (-. xRy <-> -. xRz))
19	18	cbvralv 1333	. . . . . . . . . . . . . . 15 |- (A.y e. B -. xRy <-> A.z e. B -. xRz)
20		ralnex 1209	. . . . . . . . . . . . . . 15 |- (A.z e. B -. xRz <-> -. E.z e. B xRz)
21	19, 20	bitr 151	. . . . . . . . . . . . . 14 |- (A.y e. B -. xRy <-> -. E.z e. B xRz)
22	21	bicon2i 194	. . . . . . . . . . . . 13 |- (E.z e. B xRz <-> -. A.y e. B -. xRy)
23	16, 22	syl6ib 185	. . . . . . . . . . . 12 |- ((A.y e. A (yRw -> E.z e. B yRz) /\ x e. A) -> (xRw -> -. A.y e. B -. xRy))
24	23	con2d 83	. . . . . . . . . . 11 |- ((A.y e. A (yRw -> E.z e. B yRz) /\ x e. A) -> (A.y e. B -. xRy -> -. xRw))
25	24	exp 291	. . . . . . . . . 10 |- (A.y e. A (yRw -> E.z e. B yRz) -> (x e. A -> (A.y e. B -. xRy -> -. xRw)))
26	25	a1i 7	. . . . . . . . 9 |- (A.y e. A (yRx -> E.z e. B yRz) -> (A.y e. A (yRw -> E.z e. B yRz) -> (x e. A -> (A.y e. B -. xRy -> -. xRw))))
27	26	com4t 40	. . . . . . . 8 |- (x e. A -> (A.y e. B -. xRy -> (A.y e. A (yRx -> E.z e. B yRz) -> (A.y e. A (yRw -> E.z e. B yRz) -> -. xRw))))
28	27	imp42 287	. . . . . . 7 |- (((x e. A /\ (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz))) /\ A.y e. A (yRw -> E.z e. B yRz)) -> -. xRw)
29	28	adantrl 311	. . . . . 6 |- (((x e. A /\ (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz))) /\ (A.y e. B -. wRy /\ A.y e. A (yRw -> E.z e. B yRz))) -> -. xRw)
30	29	adantrl 311	. . . . 5 |- (((x e. A /\ (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz))) /\ (w e. A /\ (A.y e. B -. wRy /\ A.y e. A (yRw -> E.z e. B yRz)))) -> -. xRw)
31		breq1 2065	. . . . . . . . . . . . . . . 16 |- (y = w -> (yRx <-> wRx))
32		breq1 2065	. . . . . . . . . . . . . . . . 17 |- (y = w -> (yRz <-> wRz))
33	32	birexdv 1220	. . . . . . . . . . . . . . . 16 |- (y = w -> (E.z e. B yRz <-> E.z e. B wRz))
34	31, 33	imbi12d 474	. . . . . . . . . . . . . . 15 |- (y = w -> ((yRx -> E.z e. B yRz) <-> (wRx -> E.z e. B wRz)))
35	34	rcla4v 1402	. . . . . . . . . . . . . 14 |- (A.y e. A (yRx -> E.z e. B yRz) -> (w e. A -> (wRx -> E.z e. B wRz)))
36	35	imp 277	. . . . . . . . . . . . 13 |- ((A.y e. A (yRx -> E.z e. B yRz) /\ w e. A) -> (wRx -> E.z e. B wRz))
37		breq2 2066	. . . . . . . . . . . . . . . . 17 |- (y = z -> (wRy <-> wRz))
38	37	negbid 463	. . . . . . . . . . . . . . . 16 |- (y = z -> (-. wRy <-> -. wRz))
39	38	cbvralv 1333	. . . . . . . . . . . . . . 15 |- (A.y e. B -. wRy <-> A.z e. B -. wRz)
40		ralnex 1209	. . . . . . . . . . . . . . 15 |- (A.z e. B -. wRz <-> -. E.z e. B wRz)
41	39, 40	bitr 151	. . . . . . . . . . . . . 14 |- (A.y e. B -. wRy <-> -. E.z e. B wRz)
42	41	bicon2i 194	. . . . . . . . . . . . 13 |- (E.z e. B wRz <-> -. A.y e. B -. wRy)
43	36, 42	syl6ib 185	. . . . . . . . . . . 12 |- ((A.y e. A (yRx -> E.z e. B yRz) /\ w e. A) -> (wRx -> -. A.y e. B -. wRy))
44	43	con2d 83	. . . . . . . . . . 11 |- ((A.y e. A (yRx -> E.z e. B yRz) /\ w e. A) -> (A.y e. B -. wRy -> -. wRx))
45	44	exp 291	. . . . . . . . . 10 |- (A.y e. A (yRx -> E.z e. B yRz) -> (w e. A -> (A.y e. B -. wRy -> -. wRx)))
46	45	a1i 7	. . . . . . . . 9 |- (A.y e. A (yRw -> E.z e. B yRz) -> (A.y e. A (yRx -> E.z e. B yRz) -> (w e. A -> (A.y e. B -. wRy -> -. wRx))))
47	46	com4l 39	. . . . . . . 8 |- (A.y e. A (yRx -> E.z e. B yRz) -> (w e. A -> (A.y e. B -. wRy -> (A.y e. A (yRw -> E.z e. B yRz) -> -. wRx))))
48	47	imp45 290	. . . . . . 7 |- ((A.y e. A (yRx -> E.z e. B yRz) /\ (w e. A /\ (A.y e. B -. wRy /\ A.y e. A (yRw -> E.z e. B yRz)))) -> -. wRx)
49	48	adantll 309	. . . . . 6 |- (((A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz)) /\ (w e. A /\ (A.y e. B -. wRy /\ A.y e. A (yRw -> E.z e. B yRz)))) -> -. wRx)
50	49	adantll 309	. . . . 5 |- (((x e. A /\ (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz))) /\ (w e. A /\ (A.y e. B -. wRy /\ A.y e. A (yRw -> E.z e. B yRz)))) -> -. wRx)
51	30, 50	jca 236	. . . 4 |- (((x e. A /\ (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz))) /\ (w e. A /\ (A.y e. B -. wRy /\ A.y e. A (yRw -> E.z e. B yRz)))) -> (-. xRw /\ -. wRx))
52		supmo.1	. . . . . . 7 |- R Or A
53		sotrieq2 2150	. . . . . . 7 |- ((R Or A /\ (x e.