Theorem supinf

Description: The supremum is the infimum of the upper bounds. (Contributed by SN, 29-Jun-2025)

	Ref	Expression
Hypotheses	supinf.1	$$⊢\phi \to \underset{\dot{}}{<}\mathrm{Or}A$$
	supinf.2	$$⊢\phi \to \exists x\in A\left(\forall y\in B\neg x\underset{\dot{}}{<}y\wedge \forall y\in A\left(y\underset{\dot{}}{<}x\to \exists z\in By\underset{\dot{}}{<}z\right)\right)$$
Assertion	supinf	$$⊢\phi \to sup\left(B,A,\underset{\dot{}}{<}\right)=inf\left(\left\{x\in A|\forall w\in B\neg x\underset{\dot{}}{<}w\right\},A,\underset{\dot{}}{<}\right)$$

Proof

Step	Hyp	Ref	Expression
1		supinf.1	$$⊢\phi \to \underset{\dot{}}{<}\mathrm{Or}A$$
2		supinf.2	$$⊢\phi \to \exists x\in A\left(\forall y\in B\neg x\underset{\dot{}}{<}y\wedge \forall y\in A\left(y\underset{\dot{}}{<}x\to \exists z\in By\underset{\dot{}}{<}z\right)\right)$$
3	1 2	supcl	$$⊢\phi \to sup\left(B,A,\underset{\dot{}}{<}\right)\in A$$
4		breq1	$$⊢x=sup\left(B,A,\underset{\dot{}}{<}\right)\to \left(x\underset{\dot{}}{<}w\leftrightarrow sup\left(B,A,\underset{\dot{}}{<}\right)\underset{\dot{}}{<}w\right)$$
5	4	notbid	$$⊢x=sup\left(B,A,\underset{\dot{}}{<}\right)\to \left(\neg x\underset{\dot{}}{<}w\leftrightarrow \neg sup\left(B,A,\underset{\dot{}}{<}\right)\underset{\dot{}}{<}w\right)$$
6	5	ralbidv	$$⊢x=sup\left(B,A,\underset{\dot{}}{<}\right)\to \left(\forall w\in B\neg x\underset{\dot{}}{<}w\leftrightarrow \forall w\in B\neg sup\left(B,A,\underset{\dot{}}{<}\right)\underset{\dot{}}{<}w\right)$$
7	1 2	supub	$$⊢\phi \to \left(v\in B\to \neg sup\left(B,A,\underset{\dot{}}{<}\right)\underset{\dot{}}{<}v\right)$$
8	7	ralrimiv	$$⊢\phi \to \forall v\in B\neg sup\left(B,A,\underset{\dot{}}{<}\right)\underset{\dot{}}{<}v$$
9		breq2	$$⊢v=w\to \left(sup\left(B,A,\underset{\dot{}}{<}\right)\underset{\dot{}}{<}v\leftrightarrow sup\left(B,A,\underset{\dot{}}{<}\right)\underset{\dot{}}{<}w\right)$$
10	9	notbid	$$⊢v=w\to \left(\neg sup\left(B,A,\underset{\dot{}}{<}\right)\underset{\dot{}}{<}v\leftrightarrow \neg sup\left(B,A,\underset{\dot{}}{<}\right)\underset{\dot{}}{<}w\right)$$
11	10	cbvralvw	$$⊢\forall v\in B\neg sup\left(B,A,\underset{\dot{}}{<}\right)\underset{\dot{}}{<}v\leftrightarrow \forall w\in B\neg sup\left(B,A,\underset{\dot{}}{<}\right)\underset{\dot{}}{<}w$$
12	8 11	sylib	$$⊢\phi \to \forall w\in B\neg sup\left(B,A,\underset{\dot{}}{<}\right)\underset{\dot{}}{<}w$$
13	6 3 12	elrabd	$$⊢\phi \to sup\left(B,A,\underset{\dot{}}{<}\right)\in \left\{x\in A|\forall w\in B\neg x\underset{\dot{}}{<}w\right\}$$
14		breq1	$$⊢x=v\to \left(x\underset{\dot{}}{<}w\leftrightarrow v\underset{\dot{}}{<}w\right)$$
15	14	notbid	$$⊢x=v\to \left(\neg x\underset{\dot{}}{<}w\leftrightarrow \neg v\underset{\dot{}}{<}w\right)$$
16	15	ralbidv	$$⊢x=v\to \left(\forall w\in B\neg x\underset{\dot{}}{<}w\leftrightarrow \forall w\in B\neg v\underset{\dot{}}{<}w\right)$$
17	16	elrab	$$⊢v\in \left\{x\in A|\forall w\in B\neg x\underset{\dot{}}{<}w\right\}\leftrightarrow \left(v\in A\wedge \forall w\in B\neg v\underset{\dot{}}{<}w\right)$$
18		breq2	$$⊢z=w\to \left(y\underset{\dot{}}{<}z\leftrightarrow y\underset{\dot{}}{<}w\right)$$
19	18	cbvrexvw	$$⊢\exists z\in By\underset{\dot{}}{<}z\leftrightarrow \exists w\in By\underset{\dot{}}{<}w$$
20	19	imbi2i	$$⊢\left(y\underset{\dot{}}{<}x\to \exists z\in By\underset{\dot{}}{<}z\right)\leftrightarrow \left(y\underset{\dot{}}{<}x\to \exists w\in By\underset{\dot{}}{<}w\right)$$
21	20	ralbii	$$⊢\forall y\in A\left(y\underset{\dot{}}{<}x\to \exists z\in By\underset{\dot{}}{<}z\right)\leftrightarrow \forall y\in A\left(y\underset{\dot{}}{<}x\to \exists w\in By\underset{\dot{}}{<}w\right)$$
22	21	anbi2i	$$⊢\left(\forall y\in B\neg x\underset{\dot{}}{<}y\wedge \forall y\in A\left(y\underset{\dot{}}{<}x\to \exists z\in By\underset{\dot{}}{<}z\right)\right)\leftrightarrow \left(\forall y\in B\neg x\underset{\dot{}}{<}y\wedge \forall y\in A\left(y\underset{\dot{}}{<}x\to \exists w\in By\underset{\dot{}}{<}w\right)\right)$$
23	22	rexbii	$$⊢\exists x\in A\left(\forall y\in B\neg x\underset{\dot{}}{<}y\wedge \forall y\in A\left(y\underset{\dot{}}{<}x\to \exists z\in By\underset{\dot{}}{<}z\right)\right)\leftrightarrow \exists x\in A\left(\forall y\in B\neg x\underset{\dot{}}{<}y\wedge \forall y\in A\left(y\underset{\dot{}}{<}x\to \exists w\in By\underset{\dot{}}{<}w\right)\right)$$
24	2 23	sylib	$$⊢\phi \to \exists x\in A\left(\forall y\in B\neg x\underset{\dot{}}{<}y\wedge \forall y\in A\left(y\underset{\dot{}}{<}x\to \exists w\in By\underset{\dot{}}{<}w\right)\right)$$
25	1 24	supnub	$$⊢\phi \to \left(\left(v\in A\wedge \forall w\in B\neg v\underset{\dot{}}{<}w\right)\to \neg v\underset{\dot{}}{<}sup\left(B,A,\underset{\dot{}}{<}\right)\right)$$
26	17 25	biimtrid	$$⊢\phi \to \left(v\in \left\{x\in A|\forall w\in B\neg x\underset{\dot{}}{<}w\right\}\to \neg v\underset{\dot{}}{<}sup\left(B,A,\underset{\dot{}}{<}\right)\right)$$
27	26	imp	$$⊢\left(\phi \wedge v\in \left\{x\in A|\forall w\in B\neg x\underset{\dot{}}{<}w\right\}\right)\to \neg v\underset{\dot{}}{<}sup\left(B,A,\underset{\dot{}}{<}\right)$$
28	1 3 13 27	infmin	$$⊢\phi \to inf\left(\left\{x\in A|\forall w\in B\neg x\underset{\dot{}}{<}w\right\},A,\underset{\dot{}}{<}\right)=sup\left(B,A,\underset{\dot{}}{<}\right)$$
29	28	eqcomd	$$⊢\phi \to sup\left(B,A,\underset{\dot{}}{<}\right)=inf\left(\left\{x\in A|\forall w\in B\neg x\underset{\dot{}}{<}w\right\},A,\underset{\dot{}}{<}\right)$$