supmo

Description: Any class B has at most one supremum in A (where R is interpreted as 'less than'). (Contributed by NM, 5-May-1999) (Revised by Mario Carneiro, 24-Dec-2016)

		Ref	Expression
	Hypothesis	supmo.1	$⊢ φ \to R Or A$
	Assertion	supmo	$⊢ φ \to \exists^{*} x \in A (\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z))$

Proof

Step	Hyp	Ref	Expression
1		supmo.1	$⊢ φ \to R Or A$
2		ancom	$⊢ (\forall y \in B \neg x R y \land \forall y \in B \neg w R y) \leftrightarrow (\forall y \in B \neg w R y \land \forall y \in B \neg x R y)$
3	2	anbi2ci	$⊢ ((\forall y \in B \neg x R y \land \forall y \in B \neg w R y) \land (\forall y \in A (y R w \to \exists z \in B y R z) \land \forall y \in A (y R x \to \exists z \in B y R z))) \leftrightarrow ((\forall y \in A (y R w \to \exists z \in B y R z) \land \forall y \in A (y R x \to \exists z \in B y R z)) \land (\forall y \in B \neg w R y \land \forall y \in B \neg x R y))$
4		an42	$⊢ ((\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z)) \land (\forall y \in B \neg w R y \land \forall y \in A (y R w \to \exists z \in B y R z))) \leftrightarrow ((\forall y \in B \neg x R y \land \forall y \in B \neg w R y) \land (\forall y \in A (y R w \to \exists z \in B y R z) \land \forall y \in A (y R x \to \exists z \in B y R z)))$
5		an42	$⊢ ((\forall y \in A (y R w \to \exists z \in B y R z) \land \forall y \in B \neg x R y) \land (\forall y \in A (y R x \to \exists z \in B y R z) \land \forall y \in B \neg w R y)) \leftrightarrow ((\forall y \in A (y R w \to \exists z \in B y R z) \land \forall y \in A (y R x \to \exists z \in B y R z)) \land (\forall y \in B \neg w R y \land \forall y \in B \neg x R y))$
6	3 4 5	3bitr4i	$⊢ ((\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z)) \land (\forall y \in B \neg w R y \land \forall y \in A (y R w \to \exists z \in B y R z))) \leftrightarrow ((\forall y \in A (y R w \to \exists z \in B y R z) \land \forall y \in B \neg x R y) \land (\forall y \in A (y R x \to \exists z \in B y R z) \land \forall y \in B \neg w R y))$
7		ralnex	$⊢ \forall y \in B \neg x R y \leftrightarrow \neg \exists y \in B x R y$
8		breq1	$⊢ y = x \to (y R w \leftrightarrow x R w)$
9		breq1	$⊢ y = x \to (y R z \leftrightarrow x R z)$
10	9	rexbidv	$⊢ y = x \to (\exists z \in B y R z \leftrightarrow \exists z \in B x R z)$
11	8 10	imbi12d	$⊢ y = x \to ((y R w \to \exists z \in B y R z) \leftrightarrow (x R w \to \exists z \in B x R z))$
12	11	rspcva	$⊢ (x \in A \land \forall y \in A (y R w \to \exists z \in B y R z)) \to (x R w \to \exists z \in B x R z)$
13		breq2	$⊢ y = z \to (x R y \leftrightarrow x R z)$
14	13	cbvrexvw	$⊢ \exists y \in B x R y \leftrightarrow \exists z \in B x R z$
15	12 14	syl6ibr	$⊢ (x \in A \land \forall y \in A (y R w \to \exists z \in B y R z)) \to (x R w \to \exists y \in B x R y)$
16	15	con3d	$⊢ (x \in A \land \forall y \in A (y R w \to \exists z \in B y R z)) \to (\neg \exists y \in B x R y \to \neg x R w)$
17	7 16	syl5bi	$⊢ (x \in A \land \forall y \in A (y R w \to \exists z \in B y R z)) \to (\forall y \in B \neg x R y \to \neg x R w)$
18	17	expimpd	$⊢ x \in A \to ((\forall y \in A (y R w \to \exists z \in B y R z) \land \forall y \in B \neg x R y) \to \neg x R w)$
19	18	ad2antrl	$⊢ (R Or A \land (x \in A \land w \in A)) \to ((\forall y \in A (y R w \to \exists z \in B y R z) \land \forall y \in B \neg x R y) \to \neg x R w)$
20		ralnex	$⊢ \forall y \in B \neg w R y \leftrightarrow \neg \exists y \in B w R y$
21		breq1	$⊢ y = w \to (y R x \leftrightarrow w R x)$
22		breq1	$⊢ y = w \to (y R z \leftrightarrow w R z)$
23	22	rexbidv	$⊢ y = w \to (\exists z \in B y R z \leftrightarrow \exists z \in B w R z)$
24	21 23	imbi12d	$⊢ y = w \to ((y R x \to \exists z \in B y R z) \leftrightarrow (w R x \to \exists z \in B w R z))$
25	24	rspcva	$⊢ (w \in A \land \forall y \in A (y R x \to \exists z \in B y R z)) \to (w R x \to \exists z \in B w R z)$
26		breq2	$⊢ y = z \to (w R y \leftrightarrow w R z)$
27	26	cbvrexvw	$⊢ \exists y \in B w R y \leftrightarrow \exists z \in B w R z$
28	25 27	syl6ibr	$⊢ (w \in A \land \forall y \in A (y R x \to \exists z \in B y R z)) \to (w R x \to \exists y \in B w R y)$
29	28	con3d	$⊢ (w \in A \land \forall y \in A (y R x \to \exists z \in B y R z)) \to (\neg \exists y \in B w R y \to \neg w R x)$
30	20 29	syl5bi	$⊢ (w \in A \land \forall y \in A (y R x \to \exists z \in B y R z)) \to (\forall y \in B \neg w R y \to \neg w R x)$
31	30	expimpd	$⊢ w \in A \to ((\forall y \in A (y R x \to \exists z \in B y R z) \land \forall y \in B \neg w R y) \to \neg w R x)$
32	31	ad2antll	$⊢ (R Or A \land (x \in A \land w \in A)) \to ((\forall y \in A (y R x \to \exists z \in B y R z) \land \forall y \in B \neg w R y) \to \neg w R x)$
33	19 32	anim12d	$⊢ (R Or A \land (x \in A \land w \in A)) \to (((\forall y \in A (y R w \to \exists z \in B y R z) \land \forall y \in B \neg x R y) \land (\forall y \in A (y R x \to \exists z \in B y R z) \land \forall y \in B \neg w R y)) \to (\neg x R w \land \neg w R x))$
34	6 33	syl5bi	$⊢ (R Or A \land (x \in A \land w \in A)) \to (((\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z)) \land (\forall y \in B \neg w R y \land \forall y \in A (y R w \to \exists z \in B y R z))) \to (\neg x R w \land \neg w R x))$
35		sotrieq2	$⊢ (R Or A \land (x \in A \land w \in A)) \to (x = w \leftrightarrow (\neg x R w \land \neg w R x))$
36	34 35	sylibrd	$⊢ (R Or A \land (x \in A \land w \in A)) \to (((\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z)) \land (\forall y \in B \neg w R y \land \forall y \in A (y R w \to \exists z \in B y R z))) \to x = w)$
37	36	ralrimivva	$⊢ R Or A \to \forall x \in A \forall w \in A (((\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z)) \land (\forall y \in B \neg w R y \land \forall y \in A (y R w \to \exists z \in B y R z))) \to x = w)$
38	1 37	syl	$⊢ φ \to \forall x \in A \forall w \in A (((\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z)) \land (\forall y \in B \neg w R y \land \forall y \in A (y R w \to \exists z \in B y R z))) \to x = w)$
39		breq1	$⊢ x = w \to (x R y \leftrightarrow w R y)$
40	39	notbid	$⊢ x = w \to (\neg x R y \leftrightarrow \neg w R y)$
41	40	ralbidv	$⊢ x = w \to (\forall y \in B \neg x R y \leftrightarrow \forall y \in B \neg w R y)$
42		breq2	$⊢ x = w \to (y R x \leftrightarrow y R w)$
43	42	imbi1d	$⊢ x = w \to ((y R x \to \exists z \in B y R z) \leftrightarrow (y R w \to \exists z \in B y R z))$
44	43	ralbidv	$⊢ x = w \to (\forall y \in A (y R x \to \exists z \in B y R z) \leftrightarrow \forall y \in A (y R w \to \exists z \in B y R z))$
45	41 44	anbi12d	$⊢ x = w \to ((\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z)) \leftrightarrow (\forall y \in B \neg w R y \land \forall y \in A (y R w \to \exists z \in B y R z)))$
46	45	rmo4	$⊢ \exists^{*} x \in A (\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z)) \leftrightarrow \forall x \in A \forall w \in A (((\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z)) \land (\forall y \in B \neg w R y \land \forall y \in A (y R w \to \exists z \in B y R z))) \to x = w)$
47	38 46	sylibr	$⊢ φ \to \exists^{*} x \in A (\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z))$

Metamath Proof Explorer

Theorem supmo

Proof