infmo

Description: Any class B has at most one infimum in A (where R is interpreted as 'less than'). (Contributed by AV, 6-Oct-2020)

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

Proof

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

Metamath Proof Explorer

Theorem infmo

Proof