Theorem supmo 4550

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 groups:   x,y,z,A   x,R,y,z   x,B,y,z

Proof of Theorem supmo

Step	Hyp	Ref	Expression
1		eleq1 1526	. . . 4 |- (x = w -> (x e. A <-> w e. A))
2		breq1 2612	. . . . . . 7 |- (x = w -> (xRy <-> wRy))
3	2	negbid 609	. . . . . 6 |- (x = w -> (-. xRy <-> -. wRy))
4	3	ralbidv 1655	. . . . 5 |- (x = w -> (A.y e. B -. xRy <-> A.y e. B -. wRy))
5		breq2 2613	. . . . . . 7 |- (x = w -> (yRx <-> yRw))
6	5	imbi1d 611	. . . . . 6 |- (x = w -> ((yRx -> E.z e. B yRz) <-> (yRw -> E.z e. B yRz)))
7	6	ralbidv 1655	. . . . 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 626	. . . 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 626	. . 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 1396	. 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 2612	. . . . . . . . . . . . . 14 |- (y = x -> (yRw <-> xRw))
12		breq1 2612	. . . . . . . . . . . . . . 15 |- (y = x -> (yRz <-> xRz))
13	12	rexbidv 1656	. . . . . . . . . . . . . 14 |- (y = x -> (E.z e. B yRz <-> E.z e. B xRz))
14	11, 13	imbi12d 624	. . . . . . . . . . . . 13 |- (y = x -> ((yRw -> E.z e. B yRz) <-> (xRw -> E.z e. B xRz)))
15	14	rcla4va 1866	. . . . . . . . . . . 12 |- ((x e. A /\ A.y e. A (yRw -> E.z e. B yRz)) -> (xRw -> E.z e. B xRz))
16	15	con3d 95	. . . . . . . . . . 11 |- ((x e. A /\ A.y e. A (yRw -> E.z e. B yRz)) -> (-. E.z e. B xRz -> -. xRw))
17	16	imp 350	. . . . . . . . . 10 |- (((x e. A /\ A.y e. A (yRw -> E.z e. B yRz)) /\ -. E.z e. B xRz) -> -. xRw)
18		breq2 2613	. . . . . . . . . . . . 13 |- (y = z -> (xRy <-> xRz))
19	18	negbid 609	. . . . . . . . . . . 12 |- (y = z -> (-. xRy <-> -. xRz))
20	19	cbvralv 1791	. . . . . . . . . . 11 |- (A.y e. B -. xRy <-> A.z e. B -. xRz)
21		ralnex 1645	. . . . . . . . . . 11 |- (A.z e. B -. xRz <-> -. E.z e. B xRz)
22	20, 21	bitr 173	. . . . . . . . . 10 |- (A.y e. B -. xRy <-> -. E.z e. B xRz)
23	17, 22	sylan2b 452	. . . . . . . . 9 |- (((x e. A /\ A.y e. A (yRw -> E.z e. B yRz)) /\ A.y e. B -. xRy) -> -. xRw)
24	23	an1rs 488	. . . . . . . 8 |- (((x e. A /\ A.y e. B -. xRy) /\ A.y e. A (yRw -> E.z e. B yRz)) -> -. xRw)
25	24	adantlrr 399	. . . . . . 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)
26	25	adantrl 394	. . . . . 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)
27	26	adantrl 394	. . . . 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)
28		breq1 2612	. . . . . . . . . . . . . 14 |- (y = w -> (yRx <-> wRx))
29		breq1 2612	. . . . . . . . . . . . . . 15 |- (y = w -> (yRz <-> wRz))
30	29	rexbidv 1656	. . . . . . . . . . . . . 14 |- (y = w -> (E.z e. B yRz <-> E.z e. B wRz))
31	28, 30	imbi12d 624	. . . . . . . . . . . . 13 |- (y = w -> ((yRx -> E.z e. B yRz) <-> (wRx -> E.z e. B wRz)))
32	31	rcla4cva 1867	. . . . . . . . . . . 12 |- ((A.y e. A (yRx -> E.z e. B yRz) /\ w e. A) -> (wRx -> E.z e. B wRz))
33	32	con3d 95	. . . . . . . . . . 11 |- ((A.y e. A (yRx -> E.z e. B yRz) /\ w e. A) -> (-. E.z e. B wRz -> -. wRx))
34	33	imp 350	. . . . . . . . . 10 |- (((A.y e. A (yRx -> E.z e. B yRz) /\ w e. A) /\ -. E.z e. B wRz) -> -. wRx)
35		breq2 2613	. . . . . . . . . . . . 13 |- (y = z -> (wRy <-> wRz))
36	35	negbid 609	. . . . . . . . . . . 12 |- (y = z -> (-. wRy <-> -. wRz))
37	36	cbvralv 1791	. . . . . . . . . . 11 |- (A.y e. B -. wRy <-> A.z e. B -. wRz)
38		ralnex 1645	. . . . . . . . . . 11 |- (A.z e. B -. wRz <-> -. E.z e. B wRz)
39	37, 38	bitr 173	. . . . . . . . . 10 |- (A.y e. B -. wRy <-> -. E.z e. B wRz)
40	34, 39	sylan2b 452	. . . . . . . . 9 |- (((A.y e. A (yRx -> E.z e. B yRz) /\ w e. A) /\ A.y e. B -. wRy) -> -. wRx)
41	40	anasss 440	. . . . . . . 8 |- ((A.y e. A (yRx -> E.z e. B yRz) /\ (w e. A /\ A.y e. B -. wRy)) -> -. wRx)
42	41	adantrrr 403	. . . . . . 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)
43	42	adantll 392	. . . . . 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)
44	43	adantll 392	. . . . 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)
45	27, 44	jca 288	. . . 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))
46		supmo.1	. . . . . 6 |- R Or A
47		sotrieq2 2853	. . . . . 6 |- ((R Or A /\ (x e. A /\ w e. A)) -> (x = w <-> (-. xRw /\ -. wRx)))
48	46, 47	mpan 693	. . . . 5 |- ((x e. A /\ w e. A) -> (x = w <-> (-. xRw /\ -. wRx)))
49	48	ad2ant2r 409	. . . 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)))) -> (x = w <-> (-. xRw /\ -. wRx)))
50	45, 49	mpbird 196	. . 3 |- (((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)
51	50	ax-gen 960	. 2 |- A.w(((x e. A /\