Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

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	⊢ ∃*x(x ∈ A ∧ (∀y ∈ B ¬ xRy ∧ ∀y ∈ A (yRx → ∃z ∈ 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 ∈ A ↔ w ∈ 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 → (∀y ∈ B ¬ xRy ↔ ∀y ∈ B ¬ wRy))
5		breq2 2066	. . . . . . 7 ⊢ (x = w → (yRx ↔ yRw))
6	5	imbi1d 465	. . . . . 6 ⊢ (x = w → ((yRx → ∃z ∈ B yRz) ↔ (yRw → ∃z ∈ B yRz)))
7	6	biraldv 1219	. . . . 5 ⊢ (x = w → (∀y ∈ A (yRx → ∃z ∈ B yRz) ↔ ∀y ∈ A (yRw → ∃z ∈ B yRz)))
8	4, 7	anbi12d 476	. . . 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 476	. . 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 1029	. 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 2065	. . . . . . . . . . . . . . . 16 ⊢ (y = x → (yRw ↔ xRw))
12		breq1 2065	. . . . . . . . . . . . . . . . 17 ⊢ (y = x → (yRz ↔ xRz))
13	12	birexdv 1220	. . . . . . . . . . . . . . . 16 ⊢ (y = x → (∃z ∈ B yRz ↔ ∃z ∈ B xRz))
14	11, 13	imbi12d 474	. . . . . . . . . . . . . . 15 ⊢ (y = x → ((yRw → ∃z ∈ B yRz) ↔ (xRw → ∃z ∈ B xRz)))
15	14	rcla4v 1402	. . . . . . . . . . . . . 14 ⊢ (∀y ∈ A (yRw → ∃z ∈ B yRz) → (x ∈ A → (xRw → ∃z ∈ B xRz)))
16	15	imp 277	. . . . . . . . . . . . 13 ⊢ ((∀y ∈ A (yRw → ∃z ∈ B yRz) ∧ x ∈ A) → (xRw → ∃z ∈ B xRz))
17		breq2 2066	. . . . . . . . . . . . . . . . 17 ⊢ (y = z → (xRy ↔ xRz))
18	17	negbid 463	. . . . . . . . . . . . . . . 16 ⊢ (y = z → (¬ xRy ↔ ¬ xRz))
19	18	cbvralv 1333	. . . . . . . . . . . . . . 15 ⊢ (∀y ∈ B ¬ xRy ↔ ∀z ∈ B ¬ xRz)
20		ralnex 1209	. . . . . . . . . . . . . . 15 ⊢ (∀z ∈ B ¬ xRz ↔ ¬ ∃z ∈ B xRz)
21	19, 20	bitr 151	. . . . . . . . . . . . . 14 ⊢ (∀y ∈ B ¬ xRy ↔ ¬ ∃z ∈ B xRz)
22	21	bicon2i 194	. . . . . . . . . . . . 13 ⊢ (∃z ∈ B xRz ↔ ¬ ∀y ∈ B ¬ xRy)
23	16, 22	syl6ib 185	. . . . . . . . . . . 12 ⊢ ((∀y ∈ A (yRw → ∃z ∈ B yRz) ∧ x ∈ A) → (xRw → ¬ ∀y ∈ B ¬ xRy))
24	23	con2d 83	. . . . . . . . . . 11 ⊢ ((∀y ∈ A (yRw → ∃z ∈ B yRz) ∧ x ∈ A) → (∀y ∈ B ¬ xRy → ¬ xRw))
25	24	exp 291	. . . . . . . . . 10 ⊢ (∀y ∈ A (yRw → ∃z ∈ B yRz) → (x ∈ A → (∀y ∈ B ¬ xRy → ¬ xRw)))
26	25	a1i 7	. . . . . . . . 9 ⊢ (∀y ∈ A (yRx → ∃z ∈ B yRz) → (∀y ∈ A (yRw → ∃z ∈ B yRz) → (x ∈ A → (∀y ∈ B ¬ xRy → ¬ xRw))))
27	26	com4t 40	. . . . . . . 8 ⊢ (x ∈ A → (∀y ∈ B ¬ xRy → (∀y ∈ A (yRx → ∃z ∈ B yRz) → (∀y ∈ A (yRw → ∃z ∈ B yRz) → ¬ xRw))))
28	27	imp42 287	. . . . . . 7 ⊢ (((x ∈ A ∧ (∀y ∈ B ¬ xRy ∧ ∀y ∈ A (yRx → ∃z ∈ B yRz))) ∧ ∀y ∈ A (yRw → ∃z ∈ B yRz)) → ¬ xRw)
29	28	adantrl 311	. . . . . 6 ⊢ (((x ∈ A ∧ (∀y ∈ B ¬ xRy ∧ ∀y ∈ A (yRx → ∃z ∈ B yRz))) ∧ (∀y ∈ B ¬ wRy ∧ ∀y ∈ A (yRw → ∃z ∈ B yRz))) → ¬ xRw)
30	29	adantrl 311	. . . . 5 ⊢ (((x ∈ A ∧ (∀y ∈ B ¬ xRy ∧ ∀y ∈ A (yRx → ∃z ∈ B yRz))) ∧ (w ∈ A ∧ (∀y ∈ B ¬ wRy ∧ ∀y ∈ A (yRw → ∃z ∈ 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 → (∃z ∈ B yRz ↔ ∃z ∈ B wRz))
34	31, 33	imbi12d 474	. . . . . . . . . . . . . . 15 ⊢ (y = w → ((yRx → ∃z ∈ B yRz) ↔ (wRx → ∃z ∈ B wRz)))
35	34	rcla4v 1402	. . . . . . . . . . . . . 14 ⊢ (∀y ∈ A (yRx → ∃z ∈ B yRz) → (w ∈ A → (wRx → ∃z ∈ B wRz)))
36	35	imp 277	. . . . . . . . . . . . 13 ⊢ ((∀y ∈ A (yRx → ∃z ∈ B yRz) ∧ w ∈ A) → (wRx → ∃z ∈ B wRz))
37		breq2 2066	. . . . . . . . . . . . . . . . 17 ⊢ (y = z → (wRy ↔ wRz))
38	37	negbid 463	. . . . . . . . . . . . . . . 16 ⊢ (y = z → (¬ wRy ↔ ¬ wRz))
39	38	cbvralv 1333	. . . . . . . . . . . . . . 15 ⊢ (∀y ∈ B ¬ wRy ↔ ∀z ∈ B ¬ wRz)
40		ralnex 1209	. . . . . . . . . . . . . . 15 ⊢ (∀z ∈ B ¬ wRz ↔ ¬ ∃z ∈ B wRz)
41	39, 40	bitr 151	. . . . . . . . . . . . . 14 ⊢ (∀y ∈ B ¬ wRy ↔ ¬ ∃z ∈ B wRz)
42	41	bicon2i 194	. . . . . . . . . . . . 13 ⊢ (∃z ∈ B wRz ↔ ¬ ∀y ∈ B ¬ wRy)
43	36, 42	syl6ib 185	. . . . . . . . . . . 12 ⊢ ((∀y ∈ A (yRx → ∃z ∈ B yRz) ∧ w ∈ A) → (wRx → ¬ ∀y ∈ B ¬ wRy))
44	43	con2d 83	. . . . . . . . . . 11 ⊢ ((∀y ∈ A (yRx → ∃z ∈ B yRz) ∧ w ∈ A) → (∀y ∈ B ¬ wRy → ¬ wRx))
45	44	exp 291	. . . . . . . . . 10 ⊢ (∀y ∈ A (yRx → ∃z ∈ B yRz) → (w ∈ A → (∀y ∈ B ¬ wRy → ¬ wRx)))
46	45	a1i 7	. . . . . . . . 9 ⊢ (∀y ∈ A (yRw → ∃z ∈ B yRz) → (∀y ∈ A (yRx → ∃z ∈ B yRz) → (w ∈ A → (∀y ∈ B ¬ wRy → ¬ wRx))))
47	46	com4l 39	. . . . . . . 8 ⊢ (∀y ∈ A (yRx → ∃z ∈ B yRz) → (w ∈ A → (∀y ∈ B ¬ wRy → (∀y ∈ A (yRw → ∃z ∈ B yRz) → ¬ wRx))))
48	47	imp45 290	. . . . . . 7 ⊢ ((∀y ∈ A (yRx → ∃z ∈ B yRz) ∧ (w ∈ A ∧ (∀y ∈ B ¬ wRy ∧ ∀y ∈ A (yRw → ∃z ∈ B yRz)))) → ¬ wRx)
49	48	adantll 309	. . . . . 6 ⊢ (((∀y ∈ B ¬ xRy ∧ ∀y ∈ A (yRx → ∃z ∈ B yRz)) ∧ (w ∈ A ∧ (∀y ∈ B ¬ wRy ∧ ∀y ∈ A (yRw → ∃z ∈ B yRz)))) → ¬ wRx)
50	49	adantll 309	. . . . 5 ⊢ (((x ∈ A ∧ (∀y ∈ B ¬ xRy ∧ ∀y ∈ A (yRx → ∃z ∈ B yRz))) ∧ (w ∈ A ∧ (∀y ∈ B ¬ wRy ∧ ∀y ∈ A (yRw → ∃z ∈ B yRz)))) → ¬ wRx)
51	30, 50	jca 236	. . . 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))
52		supmo.1	. . . . . . 7 ⊢ R Or A
53		sotrieq2 2150	. . . . . . 7 ⊢ ((R Or A ∧ (x ∈ A ∧ w ∈ A)) → (x = w ↔ (¬ xRw ∧ ¬ wRx)))
54	52, 53	mpan 518	. . . . . 6 ⊢ ((x ∈ A ∧ w ∈ A) → (x = w ↔ (¬ xRw ∧ ¬ wRx)))
55	54	adantrr 312	. . . . 5 ⊢ ((x ∈ A ∧ (w ∈ A ∧ (∀y ∈ B ¬ wRy ∧ ∀y ∈ A (yRw → ∃z ∈ B yRz)))) → (x = w ↔ (¬ xRw ∧ ¬ wRx)))
56	55	adantlr 310	. . . 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)))
57	51, 56	mpbird 171	. . 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)
58	57	ax-gen 677	. 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)
59	10, 58	mpgbir 686	1 ⊢ ∃*x(x ∈ A ∧ (∀y ∈ B ¬ xRy ∧ ∀y ∈ A (yRx → ∃z ∈ B yRz)))

Colors of variables: wff set class

Syntax hints: ¬ wn 1 → wi 2 ↔ wb 127 ∧ wa 196 ∀wal 672 = weq 797 ∃*wmo 1008 ∈ wcel 1092 ∀wral 1201 ∃wrex 1202 class class class wbr 2054 Or wor 2059

This theorem is referenced by: supex 2157 supeu 2158 supsn 2168

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-16 922 ax-17 925 ax-ext 1074

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ral 1205 df-rex 1206 df-v 1349 df-un 1490 df-sn 1811 df-pr 1812 df-op 1815 df-br 2063 df-po 2128 df-so 2138

metamath.org