Theorem supmo 4559

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	⊢ ∃*x(x ∈ A ⋀ (∀y ∈ B ¬ xRy ⋀ ∀y ∈ A (yRx → ∃z ∈ 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 1532	. . . 4 ⊢ (x = w → (x ∈ A ↔ w ∈ A))
2		breq1 2618	. . . . . . 7 ⊢ (x = w → (xRy ↔ wRy))
3	2	negbid 610	. . . . . 6 ⊢ (x = w → (¬ xRy ↔ ¬ wRy))
4	3	ralbidv 1661	. . . . 5 ⊢ (x = w → (∀y ∈ B ¬ xRy ↔ ∀y ∈ B ¬ wRy))
5		breq2 2619	. . . . . . 7 ⊢ (x = w → (yRx ↔ yRw))
6	5	imbi1d 612	. . . . . 6 ⊢ (x = w → ((yRx → ∃z ∈ B yRz) ↔ (yRw → ∃z ∈ B yRz)))
7	6	ralbidv 1661	. . . . 5 ⊢ (x = w → (∀y ∈ A (yRx → ∃z ∈ B yRz) ↔ ∀y ∈ A (yRw → ∃z ∈ B yRz)))
8	4, 7	anbi12d 627	. . . 4 ⊢ (x = w → ((∀y ∈ B ¬ xRy ⋀ ∀y ∈ A (yRx → ∃z ∈ B yRz)) ↔ (∀y ∈ B ¬ wRy ⋀ ∀y ∈ A (yRw → ∃z ∈ B yRz))))
9	1, 8	anbi12d 627	. . 3 ⊢ (x = w → ((x ∈ A ⋀ (∀y ∈ B ¬ xRy ⋀ ∀y ∈ A (yRx → ∃z ∈ B yRz))) ↔ (w ∈ A ⋀ (∀y ∈ B ¬ wRy ⋀ ∀y ∈ A (yRw → ∃z ∈ B yRz)))))
10	9	mo4 1402	. 2 ⊢ (∃*x(x ∈ A ⋀ (∀y ∈ B ¬ xRy ⋀ ∀y ∈ A (yRx → ∃z ∈ B yRz))) ↔ ∀x∀w(((x ∈ A ⋀ (∀y ∈ B ¬ xRy ⋀ ∀y ∈ A (yRx → ∃z ∈ B yRz))) ⋀ (w ∈ A ⋀ (∀y ∈ B ¬ wRy ⋀ ∀y ∈ A (yRw → ∃z ∈ B yRz)))) → x = w))
11		breq1 2618	. . . . . . . . . . . . . 14 ⊢ (y = x → (yRw ↔ xRw))
12		breq1 2618	. . . . . . . . . . . . . . 15 ⊢ (y = x → (yRz ↔ xRz))
13	12	rexbidv 1662	. . . . . . . . . . . . . 14 ⊢ (y = x → (∃z ∈ B yRz ↔ ∃z ∈ B xRz))
14	11, 13	imbi12d 625	. . . . . . . . . . . . 13 ⊢ (y = x → ((yRw → ∃z ∈ B yRz) ↔ (xRw → ∃z ∈ B xRz)))
15	14	rcla4va 1872	. . . . . . . . . . . 12 ⊢ ((x ∈ A ⋀ ∀y ∈ A (yRw → ∃z ∈ B yRz)) → (xRw → ∃z ∈ B xRz))
16	15	con3d 95	. . . . . . . . . . 11 ⊢ ((x ∈ A ⋀ ∀y ∈ A (yRw → ∃z ∈ B yRz)) → (¬ ∃z ∈ B xRz → ¬ xRw))
17	16	imp 350	. . . . . . . . . 10 ⊢ (((x ∈ A ⋀ ∀y ∈ A (yRw → ∃z ∈ B yRz)) ⋀ ¬ ∃z ∈ B xRz) → ¬ xRw)
18		breq2 2619	. . . . . . . . . . . . 13 ⊢ (y = z → (xRy ↔ xRz))
19	18	negbid 610	. . . . . . . . . . . 12 ⊢ (y = z → (¬ xRy ↔ ¬ xRz))
20	19	cbvralv 1797	. . . . . . . . . . 11 ⊢ (∀y ∈ B ¬ xRy ↔ ∀z ∈ B ¬ xRz)
21		ralnex 1651	. . . . . . . . . . 11 ⊢ (∀z ∈ B ¬ xRz ↔ ¬ ∃z ∈ B xRz)
22	20, 21	bitr 173	. . . . . . . . . 10 ⊢ (∀y ∈ B ¬ xRy ↔ ¬ ∃z ∈ B xRz)
23	17, 22	sylan2b 452	. . . . . . . . 9 ⊢ (((x ∈ A ⋀ ∀y ∈ A (yRw → ∃z ∈ B yRz)) ⋀ ∀y ∈ B ¬ xRy) → ¬ xRw)
24	23	an1rs 489	. . . . . . . 8 ⊢ (((x ∈ A ⋀ ∀y ∈ B ¬ xRy) ⋀ ∀y ∈ A (yRw → ∃z ∈ B yRz)) → ¬ xRw)
25	24	adantlrr 399	. . . . . . 7 ⊢ (((x ∈ A ⋀ (∀y ∈ B ¬ xRy ⋀ ∀y ∈ A (yRx → ∃z ∈ B yRz))) ⋀ ∀y ∈ A (yRw → ∃z ∈ B yRz)) → ¬ xRw)
26	25	adantrl 394	. . . . . 6 ⊢ (((x ∈ A ⋀ (∀y ∈ B ¬ xRy ⋀ ∀y ∈ A (yRx → ∃z ∈ B yRz))) ⋀ (∀y ∈ B ¬ wRy ⋀ ∀y ∈ A (yRw → ∃z ∈ B yRz))) → ¬ xRw)
27	26	adantrl 394	. . . . 5 ⊢ (((x ∈ A ⋀ (∀y ∈ B ¬ xRy ⋀ ∀y ∈ A (yRx → ∃z ∈ B yRz))) ⋀ (w ∈ A ⋀ (∀y ∈ B ¬ wRy ⋀ ∀y ∈ A (yRw → ∃z ∈ B yRz)))) → ¬ xRw)
28		breq1 2618	. . . . . . . . . . . . . 14 ⊢ (y = w → (yRx ↔ wRx))
29		breq1 2618	. . . . . . . . . . . . . . 15 ⊢ (y = w → (yRz ↔ wRz))
30	29	rexbidv 1662	. . . . . . . . . . . . . 14 ⊢ (y = w → (∃z ∈ B yRz ↔ ∃z ∈ B wRz))
31	28, 30	imbi12d 625	. . . . . . . . . . . . 13 ⊢ (y = w → ((yRx → ∃z ∈ B yRz) ↔ (wRx → ∃z ∈ B wRz)))
32	31	rcla4cva 1873	. . . . . . . . . . . 12 ⊢ ((∀y ∈ A (yRx → ∃z ∈ B yRz) ⋀ w ∈ A) → (wRx → ∃z ∈ B wRz))
33	32	con3d 95	. . . . . . . . . . 11 ⊢ ((∀y ∈ A (yRx → ∃z ∈ B yRz) ⋀ w ∈ A) → (¬ ∃z ∈ B wRz → ¬ wRx))
34	33	imp 350	. . . . . . . . . 10 ⊢ (((∀y ∈ A (yRx → ∃z ∈ B yRz) ⋀ w ∈ A) ⋀ ¬ ∃z ∈ B wRz) → ¬ wRx)
35		breq2 2619	. . . . . . . . . . . . 13 ⊢ (y = z → (wRy ↔ wRz))
36	35	negbid 610	. . . . . . . . . . . 12 ⊢ (y = z → (¬ wRy ↔ ¬ wRz))
37	36	cbvralv 1797	. . . . . . . . . . 11 ⊢ (∀y ∈ B ¬ wRy ↔ ∀z ∈ B ¬ wRz)
38		ralnex 1651	. . . . . . . . . . 11 ⊢ (∀z ∈ B ¬ wRz ↔ ¬ ∃z ∈ B wRz)
39	37, 38	bitr 173	. . . . . . . . . 10 ⊢ (∀y ∈ B ¬ wRy ↔ ¬ ∃z ∈ B wRz)
40	34, 39	sylan2b 452	. . . . . . . . 9 ⊢ (((∀y ∈ A (yRx → ∃z ∈ B yRz) ⋀ w ∈ A) ⋀ ∀y ∈ B ¬ wRy) → ¬ wRx)
41	40	anasss 440	. . . . . . . 8 ⊢ ((∀y ∈ A (yRx → ∃z ∈ B yRz) ⋀ (w ∈ A ⋀ ∀y ∈ B ¬ wRy)) → ¬ wRx)
42	41	adantrrr 403	. . . . . . 7 ⊢ ((∀y ∈ A (yRx → ∃z ∈ B yRz) ⋀ (w ∈ A ⋀ (∀y ∈ B ¬ wRy ⋀ ∀y ∈ A (yRw → ∃z ∈ B yRz)))) → ¬ wRx)
43	42	adantll 392	. . . . . 6 ⊢ (((∀y ∈ B ¬ xRy ⋀ ∀y ∈ A (yRx → ∃z ∈ B yRz)) ⋀ (w ∈ A ⋀ (∀y ∈ B ¬ wRy ⋀ ∀y ∈ A (yRw → ∃z ∈ B yRz)))) → ¬ wRx)
44	43	adantll 392	. . . . 5 ⊢ (((x ∈ A ⋀ (∀y ∈ B ¬ xRy ⋀ ∀y ∈ A (yRx → ∃z ∈ B yRz))) ⋀ (w ∈ A ⋀ (∀y ∈ B ¬ wRy ⋀ ∀y ∈ A (yRw → ∃z ∈ B yRz)))) → ¬ wRx)
45	27, 44	jca 288	. . . 4 ⊢ (((x ∈ A ⋀ (∀y ∈ B ¬ xRy ⋀ ∀y ∈ A (yRx → ∃z ∈ B yRz))) ⋀ (w ∈ A ⋀ (∀y ∈ B ¬ wRy ⋀ ∀y ∈ A (yRw → ∃z ∈ B yRz)))) → (¬ xRw ⋀ ¬ wRx))
46		supmo.1	. . . . . 6 ⊢ R Or A
47		sotrieq2 2858	. . . . . 6 ⊢ ((R Or A ⋀ (x ∈ A ⋀ w ∈ A)) → (x = w ↔ (¬ xRw ⋀ ¬ wRx)))
48	46, 47	mpan 694	. . . . 5 ⊢ ((x ∈ A ⋀ w ∈ A) → (x = w ↔ (¬ xRw ⋀ ¬ wRx)))
49	48	ad2ant2r 409	. . . 4 ⊢ (((x ∈ A ⋀ (∀y ∈ B ¬ xRy ⋀ ∀y ∈ A (yRx → ∃z ∈ B yRz))) ⋀ (w ∈ A ⋀ (∀y ∈ B ¬ wRy ⋀ ∀y ∈ A (yRw → ∃z ∈ B yRz)))) → (x = w ↔ (¬ xRw ⋀ ¬ wRx)))
50	45, 49	mpbird 196	. . 3 ⊢ (((x ∈ A ⋀ (∀y ∈ B ¬ xRy ⋀ ∀y ∈ A (yRx → ∃z ∈ B yRz))) ⋀ (w ∈ A ⋀ (∀y ∈ B ¬ wRy ⋀ ∀y ∈ A (yRw → ∃z ∈ B yRz)))) → x = w)
51	50	ax-gen 962	. 2 ⊢ ∀w(((x ∈ A ⋀ (∀y ∈ B ¬ xRy ⋀ ∀y ∈ A (yRx → ∃z ∈ B yRz))) ⋀ (w ∈ A ⋀ (∀y ∈ B ¬ wRy ⋀ ∀y ∈ A (yRw → ∃z ∈ B yRz)))) → x = w)
52	10, 51	mpgbir 987	1 ⊢ ∃*x(x ∈ A ⋀ (∀y ∈ B ¬ xRy ⋀ ∀y ∈ A (yRx → ∃z ∈ B yRz)))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 953   = wceq 955   ∈ wcel 957  ∃*wmo 1380  ∀wral 1643  ∃wrex 1644   class class class wbr 2615   Or wor 2835

This theorem is referenced by:  supex 4560  supeu 4561  suppr 4573  supsnALT 4575

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-11 966  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 980  df-sb 1171  df-eu 1381  df-mo 1382  df-clab 1463  df-cleq 1468  df-clel 1471  df-ral 1647  df-rex 1648  df-v 1809  df-un 2047  df-sn 2409  df-pr 2410  df-op 2413  df-br 2616  df-po 2836  df-so 2846

Copyright terms: Public domain